Metamath Proof Explorer

Theorem nfcjust

Description: Justification theorem for df-nfc . (Contributed by Mario Carneiro, 13-Oct-2016)

Ref Expression
Assertion nfcjust 
|- ( A. y F/ x y e. A <-> A. z F/ x z e. A )

Proof

Step Hyp Ref Expression
1 eleq1w 
 |-  ( y = z -> ( y e. A <-> z e. A ) )
2 1 nfbidv 
 |-  ( y = z -> ( F/ x y e. A <-> F/ x z e. A ) )
3 2 cbvalvw 
 |-  ( A. y F/ x y e. A <-> A. z F/ x z e. A )