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	⊢ ( ⟨ 𝐶 , 𝐷 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐸 ) )