This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfriotadw

Description: Deduction version of nfriota with a disjoint variable condition, which contrary to nfriotad does not require ax-13 . (Contributed by NM, 18-Feb-2013) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

Ref Expression
Hypotheses nfriotadw.1 ⊢ Ⅎ 𝑦 𝜑
nfriotadw.2 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
nfriotadw.3 ⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
Assertion nfriotadw ( 𝜑 → Ⅎ 𝑥 ( ℩ 𝑦 ∈ 𝐴 𝜓 ) )

Proof

Step Hyp Ref Expression
1 nfriotadw.1 ⊢ Ⅎ 𝑦 𝜑
2 nfriotadw.2 ⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
3 nfriotadw.3 ⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
4 df-riota ⊢ ( ℩ 𝑦 ∈ 𝐴 𝜓 ) = ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) )
5 nfnaew ⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
6 1 5 nfan ⊢ Ⅎ 𝑦 ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 )
7 nfcvd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 )
8 7 adantl ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝑦 )
9 3 adantr ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝐴 )
10 8 9 nfeld ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝑦 ∈ 𝐴 )
11 2 adantr ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 𝜓 )
12 10 11 nfand ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) )
13 6 12 nfiotadw ⊢ ( ( 𝜑 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → Ⅎ 𝑥 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
14 13 ex ⊢ ( 𝜑 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ) )
15 nfiota1 ⊢ Ⅎ 𝑦 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) )
16 biidd ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑤 ∈ ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ↔ 𝑤 ∈ ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ) )
17 16 drnf1v ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( Ⅎ 𝑥 𝑤 ∈ ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ↔ Ⅎ 𝑦 𝑤 ∈ ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ) )
18 17 albidv ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑤 Ⅎ 𝑥 𝑤 ∈ ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ∀ 𝑤 Ⅎ 𝑦 𝑤 ∈ ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ) )
19 df-nfc ⊢ ( Ⅎ 𝑥 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ∀ 𝑤 Ⅎ 𝑥 𝑤 ∈ ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
20 df-nfc ⊢ ( Ⅎ 𝑦 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ↔ ∀ 𝑤 Ⅎ 𝑦 𝑤 ∈ ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
21 18 19 20 3bitr4g ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( Ⅎ 𝑥 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ↔ Ⅎ 𝑦 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) ) )
22 15 21 mpbiri ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
23 14 22 pm2.61d2 ⊢ ( 𝜑 → Ⅎ 𝑥 ( ℩ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
24 4 23 nfcxfrd ⊢ ( 𝜑 → Ⅎ 𝑥 ( ℩ 𝑦 ∈ 𝐴 𝜓 ) )