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

Metamath Proof Explorer

Theorem nfopd

Description: Deduction version of bound-variable hypothesis builder nfop . This shows how the deduction version of a not-free theorem such as nfop can be created from the corresponding not-free inference theorem. (Contributed by NM, 4-Feb-2008)

Ref Expression
Hypotheses nfopd.2 
|- ( ph -> F/_ x A )
nfopd.3 
|- ( ph -> F/_ x B )
Assertion nfopd 
|- ( ph -> F/_ x <. A , B >. )

Proof

Step Hyp Ref Expression
1 nfopd.2 
 |-  ( ph -> F/_ x A )
2 nfopd.3 
 |-  ( ph -> F/_ x B )
3 nfaba1 
 |-  F/_ x { z | A. x z e. A }
4 nfaba1 
 |-  F/_ x { z | A. x z e. B }
5 3 4 nfop 
 |-  F/_ x <. { z | A. x z e. A } , { z | A. x z e. B } >.
6 nfnfc1 
 |-  F/ x F/_ x A
7 nfnfc1 
 |-  F/ x F/_ x B
8 6 7 nfan 
 |-  F/ x ( F/_ x A /\ F/_ x B )
9 abidnf 
 |-  ( F/_ x A -> { z | A. x z e. A } = A )
10 9 adantr 
 |-  ( ( F/_ x A /\ F/_ x B ) -> { z | A. x z e. A } = A )
11 abidnf 
 |-  ( F/_ x B -> { z | A. x z e. B } = B )
12 11 adantl 
 |-  ( ( F/_ x A /\ F/_ x B ) -> { z | A. x z e. B } = B )
13 10 12 opeq12d 
 |-  ( ( F/_ x A /\ F/_ x B ) -> <. { z | A. x z e. A } , { z | A. x z e. B } >. = <. A , B >. )
14 8 13 nfceqdf 
 |-  ( ( F/_ x A /\ F/_ x B ) -> ( F/_ x <. { z | A. x z e. A } , { z | A. x z e. B } >. <-> F/_ x <. A , B >. ) )
15 1 2 14 syl2anc 
 |-  ( ph -> ( F/_ x <. { z | A. x z e. A } , { z | A. x z e. B } >. <-> F/_ x <. A , B >. ) )
16 5 15 mpbii 
 |-  ( ph -> F/_ x <. A , B >. )