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

Metamath Proof Explorer

Theorem nfnfc

Description: Hypothesis builder for F/_ y A . (Contributed by Mario Carneiro, 11-Aug-2016) Remove dependency on ax-13 . (Revised by Wolf Lammen, 10-Dec-2019)

Ref Expression
Hypothesis nfnfc.1 ⊢ Ⅎ 𝑥 𝐴
Assertion nfnfc Ⅎ 𝑥 Ⅎ 𝑦 𝐴

Proof

Step Hyp Ref Expression
1 nfnfc.1 ⊢ Ⅎ 𝑥 𝐴
2 df-nfc ⊢ ( Ⅎ 𝑦 𝐴 ↔ ∀ 𝑧 Ⅎ 𝑦 𝑧 ∈ 𝐴 )
3 df-nfc ⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑧 Ⅎ 𝑥 𝑧 ∈ 𝐴 )
4 1 3 mpbi ⊢ ∀ 𝑧 Ⅎ 𝑥 𝑧 ∈ 𝐴
5 4 spi ⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
6 5 nfnf ⊢ Ⅎ 𝑥 Ⅎ 𝑦 𝑧 ∈ 𝐴
7 6 nfal ⊢ Ⅎ 𝑥 ∀ 𝑧 Ⅎ 𝑦 𝑧 ∈ 𝐴
8 2 7 nfxfr ⊢ Ⅎ 𝑥 Ⅎ 𝑦 𝐴