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 ⊢ Ⅎ y φ
nfriotadw.2 ⊢ φ → Ⅎ x ψ
nfriotadw.3 ⊢ φ → Ⅎ _ x A
Assertion nfriotadw ⊢ φ → Ⅎ _ x ι y ∈ A | ψ

Proof

Step Hyp Ref Expression
1 nfriotadw.1 ⊢ Ⅎ y φ
2 nfriotadw.2 ⊢ φ → Ⅎ x ψ
3 nfriotadw.3 ⊢ φ → Ⅎ _ x A
4 df-riota ⊢ ι y ∈ A | ψ = ι y | y ∈ A ∧ ψ
5 nfnaew ⊢ Ⅎ y ¬ ∀ x x = y
6 1 5 nfan ⊢ Ⅎ y φ ∧ ¬ ∀ x x = y
7 nfcvd ⊢ ¬ ∀ x x = y → Ⅎ _ x y
8 7 adantl ⊢ φ ∧ ¬ ∀ x x = y → Ⅎ _ x y
9 3 adantr ⊢ φ ∧ ¬ ∀ x x = y → Ⅎ _ x A
10 8 9 nfeld ⊢ φ ∧ ¬ ∀ x x = y → Ⅎ x y ∈ A
11 2 adantr ⊢ φ ∧ ¬ ∀ x x = y → Ⅎ x ψ
12 10 11 nfand ⊢ φ ∧ ¬ ∀ x x = y → Ⅎ x y ∈ A ∧ ψ
13 6 12 nfiotadw ⊢ φ ∧ ¬ ∀ x x = y → Ⅎ _ x ι y | y ∈ A ∧ ψ
14 13 ex ⊢ φ → ¬ ∀ x x = y → Ⅎ _ x ι y | y ∈ A ∧ ψ
15 nfiota1 ⊢ Ⅎ _ y ι y | y ∈ A ∧ ψ
16 biidd ⊢ ∀ x x = y → w ∈ ι y | y ∈ A ∧ ψ ↔ w ∈ ι y | y ∈ A ∧ ψ
17 16 drnf1v ⊢ ∀ x x = y → Ⅎ x w ∈ ι y | y ∈ A ∧ ψ ↔ Ⅎ y w ∈ ι y | y ∈ A ∧ ψ
18 17 albidv ⊢ ∀ x x = y → ∀ w Ⅎ x w ∈ ι y | y ∈ A ∧ ψ ↔ ∀ w Ⅎ y w ∈ ι y | y ∈ A ∧ ψ
19 df-nfc ⊢ Ⅎ _ x ι y | y ∈ A ∧ ψ ↔ ∀ w Ⅎ x w ∈ ι y | y ∈ A ∧ ψ
20 df-nfc ⊢ Ⅎ _ y ι y | y ∈ A ∧ ψ ↔ ∀ w Ⅎ y w ∈ ι y | y ∈ A ∧ ψ
21 18 19 20 3bitr4g ⊢ ∀ x x = y → Ⅎ _ x ι y | y ∈ A ∧ ψ ↔ Ⅎ _ y ι y | y ∈ A ∧ ψ
22 15 21 mpbiri ⊢ ∀ x x = y → Ⅎ _ x ι y | y ∈ A ∧ ψ
23 14 22 pm2.61d2 ⊢ φ → Ⅎ _ x ι y | y ∈ A ∧ ψ
24 4 23 nfcxfrd ⊢ φ → Ⅎ _ x ι y ∈ A | ψ