Theorem relopabVD

Description: Virtual deduction proof of relopab . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. relopab is relopabVD without virtual deductions and was automatically derived from relopabVD .

	Ref	Expression
Assertion	relopabVD	⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		vex	⊢ 𝑦 ∈ V
3	1 2	pm3.2i	⊢ ( 𝑥 ∈ V ∧ 𝑦 ∈ V )
4	3	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) )
5	4	ssopab2i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) }
6	3	biantru	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) )
7	6	exbii	⊢ ( ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) )
8	7	exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) )
9	8	abbii	⊢ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) }
10		ax6ev	⊢ ∃ 𝑢 𝑢 = 𝑥
11		equcom	⊢ ( 𝑢 = 𝑥 ↔ 𝑥 = 𝑢 )
12	11	exbii	⊢ ( ∃ 𝑢 𝑢 = 𝑥 ↔ ∃ 𝑢 𝑥 = 𝑢 )
13	10 12	mpbi	⊢ ∃ 𝑢 𝑥 = 𝑢
14		ax6ev	⊢ ∃ 𝑣 𝑣 = 𝑦
15		equcom	⊢ ( 𝑣 = 𝑦 ↔ 𝑦 = 𝑣 )
16	15	exbii	⊢ ( ∃ 𝑣 𝑣 = 𝑦 ↔ ∃ 𝑣 𝑦 = 𝑣 )
17	14 16	mpbi	⊢ ∃ 𝑣 𝑦 = 𝑣
18		idn1	⊢ (    𝑦 = 𝑣    ▶    𝑦 = 𝑣    )
19		opeq2	⊢ ( 𝑦 = 𝑣 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑣 ⟩ )
20	18 19	e1a	⊢ (    𝑦 = 𝑣    ▶    ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑣 ⟩    )
21		idn2	⊢ (    𝑦 = 𝑣    ,    𝑥 = 𝑢    ▶    𝑥 = 𝑢    )
22		opeq1	⊢ ( 𝑥 = 𝑢 → ⟨ 𝑥 , 𝑣 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ )
23	21 22	e2	⊢ (    𝑦 = 𝑣    ,    𝑥 = 𝑢    ▶    ⟨ 𝑥 , 𝑣 ⟩ = ⟨ 𝑢 , 𝑣 ⟩    )
24		eqeq1	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑣 ⟩ → ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ↔ ⟨ 𝑥 , 𝑣 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ) )
25	24	biimprd	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑣 ⟩ → ( ⟨ 𝑥 , 𝑣 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ) )
26	20 23 25	e12	⊢ (    𝑦 = 𝑣    ,    𝑥 = 𝑢    ▶    ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑢 , 𝑣 ⟩    )
27		eqeq2	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) )
28	27	biimpd	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) )
29	26 28	e2	⊢ (    𝑦 = 𝑣    ,    𝑥 = 𝑢    ▶    ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ )    )
30	29	in2	⊢ (    𝑦 = 𝑣    ▶    ( 𝑥 = 𝑢 → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) )    )
31	30	in1	⊢ ( 𝑦 = 𝑣 → ( 𝑥 = 𝑢 → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) ) )
32	31	eximi	⊢ ( ∃ 𝑣 𝑦 = 𝑣 → ∃ 𝑣 ( 𝑥 = 𝑢 → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) ) )
33	17 32	ax-mp	⊢ ∃ 𝑣 ( 𝑥 = 𝑢 → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) )
34	33	19.37iv	⊢ ( 𝑥 = 𝑢 → ∃ 𝑣 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) )
35		19.37v	⊢ ( ∃ 𝑣 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) ↔ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) )
36	35	biimpi	⊢ ( ∃ 𝑣 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) )
37	34 36	syl	⊢ ( 𝑥 = 𝑢 → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) )
38	37	eximi	⊢ ( ∃ 𝑢 𝑥 = 𝑢 → ∃ 𝑢 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) )
39	13 38	ax-mp	⊢ ∃ 𝑢 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ )
40	39	19.37iv	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ )
41	40	eximi	⊢ ( ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑦 ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ )
42		19.9v	⊢ ( ∃ 𝑦 ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ↔ ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ )
43	42	biimpi	⊢ ( ∃ 𝑦 ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ )
44	41 43	syl	⊢ ( ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ )
45	44	eximi	⊢ ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑥 ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ )
46		19.9v	⊢ ( ∃ 𝑥 ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ↔ ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ )
47	46	biimpi	⊢ ( ∃ 𝑥 ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ )
48	45 47	syl	⊢ ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ )
49	48	ss2abi	⊢ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ } ⊆ { 𝑧 ∣ ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ }
50	9 49	eqsstrri	⊢ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) } ⊆ { 𝑧 ∣ ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ }
51		vex	⊢ 𝑢 ∈ V
52		vex	⊢ 𝑣 ∈ V
53	51 52	pm3.2i	⊢ ( 𝑢 ∈ V ∧ 𝑣 ∈ V )
54	53	biantru	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ↔ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) ) )
55	54	exbii	⊢ ( ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ↔ ∃ 𝑣 ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) ) )
56	55	exbii	⊢ ( ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ↔ ∃ 𝑢 ∃ 𝑣 ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) ) )
57	56	abbii	⊢ { 𝑧 ∣ ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ } = { 𝑧 ∣ ∃ 𝑢 ∃ 𝑣 ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) ) }
58	50 57	sseqtri	⊢ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) } ⊆ { 𝑧 ∣ ∃ 𝑢 ∃ 𝑣 ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) ) }
59		df-opab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) }
60		df-opab	⊢ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) } = { 𝑧 ∣ ∃ 𝑢 ∃ 𝑣 ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) ) }
61	58 59 60	3sstr4i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) } ⊆ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) }
62		df-xp	⊢ ( V × V ) = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) }
63	62	eqcomi	⊢ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) } = ( V × V )
64	61 63	sseqtri	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) } ⊆ ( V × V )
65	5 64	sstri	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ ( V × V )
66		df-rel	⊢ ( Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ ( V × V ) )
67	66	biimpri	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ ( V × V ) → Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
68	65 67	e0a	⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }