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

Metamath Proof Explorer

Theorem opeliunxp2f

Description: Membership in a union of Cartesian products, using bound-variable hypothesis for E instead of distinct variable conditions as in opeliunxp2 . (Contributed by AV, 25-Oct-2020)

Ref Expression
Hypotheses opeliunxp2f.f 
|- F/_ x E
opeliunxp2f.e 
|- ( x = C -> B = E )
Assertion opeliunxp2f 
|- ( <. C , D >. e. U_ x e. A ( { x } X. B ) <-> ( C e. A /\ D e. E ) )

Proof

Step Hyp Ref Expression
1 opeliunxp2f.f 
 |-  F/_ x E
2 opeliunxp2f.e 
 |-  ( x = C -> B = E )
3 df-br 
 |-  ( C U_ x e. A ( { x } X. B ) D <-> <. C , D >. e. U_ x e. A ( { x } X. B ) )
4 relxp 
 |-  Rel ( { x } X. B )
5 4 rgenw 
 |-  A. x e. A Rel ( { x } X. B )
6 reliun 
 |-  ( Rel U_ x e. A ( { x } X. B ) <-> A. x e. A Rel ( { x } X. B ) )
7 5 6 mpbir 
 |-  Rel U_ x e. A ( { x } X. B )
8 7 brrelex1i 
 |-  ( C U_ x e. A ( { x } X. B ) D -> C e. _V )
9 3 8 sylbir 
 |-  ( <. C , D >. e. U_ x e. A ( { x } X. B ) -> C e. _V )
10 elex 
 |-  ( C e. A -> C e. _V )
11 10 adantr 
 |-  ( ( C e. A /\ D e. E ) -> C e. _V )
12 nfiu1 
 |-  F/_ x U_ x e. A ( { x } X. B )
13 12 nfel2 
 |-  F/ x <. C , D >. e. U_ x e. A ( { x } X. B )
14 nfv 
 |-  F/ x C e. A
15 1 nfel2 
 |-  F/ x D e. E
16 14 15 nfan 
 |-  F/ x ( C e. A /\ D e. E )
17 13 16 nfbi 
 |-  F/ x ( <. C , D >. e. U_ x e. A ( { x } X. B ) <-> ( C e. A /\ D e. E ) )
18 opeq1 
 |-  ( x = C -> <. x , D >. = <. C , D >. )
19 18 eleq1d 
 |-  ( x = C -> ( <. x , D >. e. U_ x e. A ( { x } X. B ) <-> <. C , D >. e. U_ x e. A ( { x } X. B ) ) )
20 eleq1 
 |-  ( x = C -> ( x e. A <-> C e. A ) )
21 2 eleq2d 
 |-  ( x = C -> ( D e. B <-> D e. E ) )
22 20 21 anbi12d 
 |-  ( x = C -> ( ( x e. A /\ D e. B ) <-> ( C e. A /\ D e. E ) ) )
23 19 22 bibi12d 
 |-  ( x = C -> ( ( <. x , D >. e. U_ x e. A ( { x } X. B ) <-> ( x e. A /\ D e. B ) ) <-> ( <. C , D >. e. U_ x e. A ( { x } X. B ) <-> ( C e. A /\ D e. E ) ) ) )
24 opeliunxp 
 |-  ( <. x , D >. e. U_ x e. A ( { x } X. B ) <-> ( x e. A /\ D e. B ) )
25 17 23 24 vtoclg1f 
 |-  ( C e. _V -> ( <. C , D >. e. U_ x e. A ( { x } X. B ) <-> ( C e. A /\ D e. E ) ) )
26 9 11 25 pm5.21nii 
 |-  ( <. C , D >. e. U_ x e. A ( { x } X. B ) <-> ( C e. A /\ D e. E ) )