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 ⊢ Ⅎ _ x A
Assertion nfnfc ⊢ Ⅎ x Ⅎ _ y A

Proof

Step Hyp Ref Expression
1 nfnfc.1 ⊢ Ⅎ _ x A
2 df-nfc ⊢ Ⅎ _ y A ↔ ∀ z Ⅎ y z ∈ A
3 df-nfc ⊢ Ⅎ _ x A ↔ ∀ z Ⅎ x z ∈ A
4 1 3 mpbi ⊢ ∀ z Ⅎ x z ∈ A
5 4 spi ⊢ Ⅎ x z ∈ A
6 5 nfnf ⊢ Ⅎ x Ⅎ y z ∈ A
7 6 nfal ⊢ Ⅎ x ∀ z Ⅎ y z ∈ A
8 2 7 nfxfr ⊢ Ⅎ x Ⅎ _ y A