Theorem oprabv

Description: If a pair and a class are in a relationship given by a class abstraction of a collection of nested ordered pairs, the involved classes are sets. (Contributed by Alexander van der Vekens, 8-Jul-2018)

	Ref	Expression
Assertion	oprabv	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑍 → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		reloprab	⊢ Rel { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 }
2	1	brrelex12i	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑍 → ( ⟨ 𝑋 , 𝑌 ⟩ ∈ V ∧ 𝑍 ∈ V ) )
3		df-br	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑍 ↔ ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } )
4		opex	⊢ ⟨ 𝑋 , 𝑌 ⟩ ∈ V
5		nfcv	⊢ Ⅎ 𝑤 ⟨ 𝑋 , 𝑌 ⟩
6	5	nfeq1	⊢ Ⅎ 𝑤 ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩
7		nfv	⊢ Ⅎ 𝑤 𝜑
8	6 7	nfan	⊢ Ⅎ 𝑤 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
9	8	nfex	⊢ Ⅎ 𝑤 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
10	9	nfex	⊢ Ⅎ 𝑤 ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 )
11		nfcv	⊢ Ⅎ 𝑧 ⟨ 𝑋 , 𝑌 ⟩
12	11	nfeq1	⊢ Ⅎ 𝑧 ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩
13		nfsbc1v	⊢ Ⅎ 𝑧 [ 𝑍 / 𝑧 ] 𝜑
14	12 13	nfan	⊢ Ⅎ 𝑧 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 )
15	14	nfex	⊢ Ⅎ 𝑧 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 )
16	15	nfex	⊢ Ⅎ 𝑧 ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 )
17		eqeq1	⊢ ( 𝑤 = ⟨ 𝑋 , 𝑌 ⟩ → ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
18	17	anbi1d	⊢ ( 𝑤 = ⟨ 𝑋 , 𝑌 ⟩ → ( ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
19	18	2exbidv	⊢ ( 𝑤 = ⟨ 𝑋 , 𝑌 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
20		sbceq1a	⊢ ( 𝑧 = 𝑍 → ( 𝜑 ↔ [ 𝑍 / 𝑧 ] 𝜑 ) )
21	20	anbi2d	⊢ ( 𝑧 = 𝑍 → ( ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 ) ) )
22	21	2exbidv	⊢ ( 𝑧 = 𝑍 → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 ) ) )
23	10 16 19 22	opelopabgf	⊢ ( ( ⟨ 𝑋 , 𝑌 ⟩ ∈ V ∧ 𝑍 ∈ V ) → ( ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 ) ) )
24	4 23	mpan	⊢ ( 𝑍 ∈ V → ( ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 ) ) )
25		eqcom	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
26		vex	⊢ 𝑥 ∈ V
27		vex	⊢ 𝑦 ∈ V
28	26 27	opth	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ ↔ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) )
29	25 28	bitri	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) )
30		eqvisset	⊢ ( 𝑥 = 𝑋 → 𝑋 ∈ V )
31		eqvisset	⊢ ( 𝑦 = 𝑌 → 𝑌 ∈ V )
32	30 31	anim12i	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
33	29 32	sylbi	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
34	33	adantr	⊢ ( ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
35	34	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) )
36	35	anim1i	⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 ) ∧ 𝑍 ∈ V ) → ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ 𝑍 ∈ V ) )
37		df-3an	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) ↔ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) ∧ 𝑍 ∈ V ) )
38	36 37	sylibr	⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 ) ∧ 𝑍 ∈ V ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) )
39	38	expcom	⊢ ( 𝑍 ∈ V → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑋 , 𝑌 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ [ 𝑍 / 𝑧 ] 𝜑 ) → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) ) )
40	24 39	sylbid	⊢ ( 𝑍 ∈ V → ( ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) ) )
41	40	com12	⊢ ( ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ∈ { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } → ( 𝑍 ∈ V → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) ) )
42		dfoprab2	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { ⟨ 𝑤 , 𝑧 ⟩ ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
43	41 42	eleq2s	⊢ ( ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } → ( 𝑍 ∈ V → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) ) )
44	3 43	sylbi	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑍 → ( 𝑍 ∈ V → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) ) )
45	44	com12	⊢ ( 𝑍 ∈ V → ( ⟨ 𝑋 , 𝑌 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑍 → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) ) )
46	45	adantl	⊢ ( ( ⟨ 𝑋 , 𝑌 ⟩ ∈ V ∧ 𝑍 ∈ V ) → ( ⟨ 𝑋 , 𝑌 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑍 → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) ) )
47	2 46	mpcom	⊢ ( ⟨ 𝑋 , 𝑌 ⟩ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } 𝑍 → ( 𝑋 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ V ) )