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

Metamath Proof Explorer

Theorem nfdisj

Description: Bound-variable hypothesis builder for disjoint collection. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfdisjw when possible. (Contributed by Mario Carneiro, 14-Nov-2016) (New usage is discouraged.)

Ref Expression
Hypotheses nfdisj.1 
|- F/_ y A
nfdisj.2 
|- F/_ y B
Assertion nfdisj 
|- F/ y Disj_ x e. A B

Proof

Step Hyp Ref Expression
1 nfdisj.1 
 |-  F/_ y A
2 nfdisj.2 
 |-  F/_ y B
3 dfdisj2 
 |-  ( Disj_ x e. A B <-> A. z E* x ( x e. A /\ z e. B ) )
4 nftru 
 |-  F/ x T.
5 nfcvf 
 |-  ( -. A. y y = x -> F/_ y x )
6 1 a1i 
 |-  ( -. A. y y = x -> F/_ y A )
7 5 6 nfeld 
 |-  ( -. A. y y = x -> F/ y x e. A )
8 2 nfcri 
 |-  F/ y z e. B
9 8 a1i 
 |-  ( -. A. y y = x -> F/ y z e. B )
10 7 9 nfand 
 |-  ( -. A. y y = x -> F/ y ( x e. A /\ z e. B ) )
11 10 adantl 
 |-  ( ( T. /\ -. A. y y = x ) -> F/ y ( x e. A /\ z e. B ) )
12 4 11 nfmod2 
 |-  ( T. -> F/ y E* x ( x e. A /\ z e. B ) )
13 12 mptru 
 |-  F/ y E* x ( x e. A /\ z e. B )
14 13 nfal 
 |-  F/ y A. z E* x ( x e. A /\ z e. B )
15 3 14 nfxfr 
 |-  F/ y Disj_ x e. A B