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 ⊢ Ⅎ 𝑥 𝐸
opeliunxp2f.e ⊢ ( 𝑥 = 𝐶 → 𝐵 = 𝐸 )
Assertion opeliunxp2f ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 opeliunxp2f.f ⊢ Ⅎ 𝑥 𝐸
2 opeliunxp2f.e ⊢ ( 𝑥 = 𝐶 → 𝐵 = 𝐸 )
3 df-br ⊢ ( 𝐶 ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) 𝐷 ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) )
4 relxp ⊢ Rel ( { 𝑥 } × 𝐵 )
5 4 rgenw ⊢ ∀ 𝑥 ∈ 𝐴 Rel ( { 𝑥 } × 𝐵 )
6 reliun ⊢ ( Rel ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 Rel ( { 𝑥 } × 𝐵 ) )
7 5 6 mpbir ⊢ Rel ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
8 7 brrelex1i ⊢ ( 𝐶 ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) 𝐷 → 𝐶 ∈ V )
9 3 8 sylbir ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) → 𝐶 ∈ V )
10 elex ⊢ ( 𝐶 ∈ 𝐴 → 𝐶 ∈ V )
11 10 adantr ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸 ) → 𝐶 ∈ V )
12 nfiu1 ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
13 12 nfel2 ⊢ Ⅎ 𝑥 ⟨ 𝐶 , 𝐷 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
14 nfv ⊢ Ⅎ 𝑥 𝐶 ∈ 𝐴
15 1 nfel2 ⊢ Ⅎ 𝑥 𝐷 ∈ 𝐸
16 14 15 nfan ⊢ Ⅎ 𝑥 ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸 )
17 13 16 nfbi ⊢ Ⅎ 𝑥 ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸 ) )
18 opeq1 ⊢ ( 𝑥 = 𝐶 → ⟨ 𝑥 , 𝐷 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
19 18 eleq1d ⊢ ( 𝑥 = 𝐶 → ( ⟨ 𝑥 , 𝐷 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ⟨ 𝐶 , 𝐷 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) )
20 eleq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
21 2 eleq2d ⊢ ( 𝑥 = 𝐶 → ( 𝐷 ∈ 𝐵 ↔ 𝐷 ∈ 𝐸 ) )
22 20 21 anbi12d ⊢ ( 𝑥 = 𝐶 → ( ( 𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸 ) ) )
23 19 22 bibi12d ⊢ ( 𝑥 = 𝐶 → ( ( ⟨ 𝑥 , 𝐷 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) ) ↔ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸 ) ) ) )
24 opeliunxp ⊢ ( ⟨ 𝑥 , 𝐷 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) )
25 17 23 24 vtoclg1f ⊢ ( 𝐶 ∈ V → ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸 ) ) )
26 9 11 25 pm5.21nii ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸 ) )