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

Metamath Proof Explorer

Theorem nfriotad

Description: Deduction version of nfriota . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfriotadw when possible. (Contributed by NM, 18-Feb-2013) (Revised by Mario Carneiro, 15-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses nfriotad.1 ⊢ Ⅎ y φ
nfriotad.2 ⊢ φ → Ⅎ x ψ
nfriotad.3 ⊢ φ → Ⅎ _ x A
Assertion nfriotad ⊢ φ → Ⅎ _ x ι y ∈ A | ψ

Proof

Step Hyp Ref Expression
1 nfriotad.1 ⊢ Ⅎ y φ
2 nfriotad.2 ⊢ φ → Ⅎ x ψ
3 nfriotad.3 ⊢ φ → Ⅎ _ x A
4 df-riota ⊢ ι y ∈ A | ψ = ι y | y ∈ A ∧ ψ
5 nfnae ⊢ Ⅎ y ¬ ∀ x x = y
6 1 5 nfan ⊢ Ⅎ y φ ∧ ¬ ∀ x x = y
7 nfcvf ⊢ ¬ ∀ 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 nfiotad ⊢ φ ∧ ¬ ∀ x x = y → Ⅎ _ x ι y | y ∈ A ∧ ψ
14 13 ex ⊢ φ → ¬ ∀ x x = y → Ⅎ _ x ι y | y ∈ A ∧ ψ
15 nfiota1 ⊢ Ⅎ _ y ι y | y ∈ A ∧ ψ
16 eqidd ⊢ ∀ x x = y → ι y | y ∈ A ∧ ψ = ι y | y ∈ A ∧ ψ
17 16 drnfc1 ⊢ ∀ x x = y → Ⅎ _ x ι y | y ∈ A ∧ ψ ↔ Ⅎ _ y ι y | y ∈ A ∧ ψ
18 15 17 mpbiri ⊢ ∀ x x = y → Ⅎ _ x ι y | y ∈ A ∧ ψ
19 14 18 pm2.61d2 ⊢ φ → Ⅎ _ x ι y | y ∈ A ∧ ψ
20 4 19 nfcxfrd ⊢ φ → Ⅎ _ x ι y ∈ A | ψ