Theorem relopabi

Description: A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013) Remove dependency on ax-sep , ax-nul , ax-pr . (Revised by KP, 25-Oct-2021) Avoid ax-11 and ax-12 . (Revised by SN, 26-Oct-2026)

	Ref	Expression
Hypothesis	relopabi.1	⊢ 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
Assertion	relopabi	⊢ Rel 𝐴

Proof

Step	Hyp	Ref	Expression
1		relopabi.1	⊢ 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
2		vex	⊢ 𝑥 ∈ V
3		vex	⊢ 𝑦 ∈ V
4	2 3	pm3.2i	⊢ ( 𝑥 ∈ V ∧ 𝑦 ∈ V )
5	4	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) )
6	5	ssopab2i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) }
7		ax6evr	⊢ ∃ 𝑢 𝑥 = 𝑢
8		ax6evr	⊢ ∃ 𝑣 𝑦 = 𝑣
9		opeq12	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ )
10	9	eqeq2d	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) )
11	10	biimpd	⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) )
12	11	ex	⊢ ( 𝑥 = 𝑢 → ( 𝑦 = 𝑣 → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) ) )
13	12	eximdv	⊢ ( 𝑥 = 𝑢 → ( ∃ 𝑣 𝑦 = 𝑣 → ∃ 𝑣 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) ) )
14	8 13	mpi	⊢ ( 𝑥 = 𝑢 → ∃ 𝑣 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) )
15		19.37imv	⊢ ( ∃ 𝑣 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) )
16	14 15	syl	⊢ ( 𝑥 = 𝑢 → ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ) )
17	7 16	eximii	⊢ ∃ 𝑢 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ )
18	17	19.37iv	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ )
19	18	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ )
20	19	ss2abi	⊢ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ } ⊆ { 𝑧 ∣ ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ }
21	4	biantru	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) )
22	21	2exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) )
23	22	abbii	⊢ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) }
24		vex	⊢ 𝑢 ∈ V
25		vex	⊢ 𝑣 ∈ V
26	24 25	pm3.2i	⊢ ( 𝑢 ∈ V ∧ 𝑣 ∈ V )
27	26	biantru	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ↔ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) ) )
28	27	2exbii	⊢ ( ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ↔ ∃ 𝑢 ∃ 𝑣 ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) ) )
29	28	abbii	⊢ { 𝑧 ∣ ∃ 𝑢 ∃ 𝑣 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ } = { 𝑧 ∣ ∃ 𝑢 ∃ 𝑣 ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) ) }
30	20 23 29	3sstr3i	⊢ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) } ⊆ { 𝑧 ∣ ∃ 𝑢 ∃ 𝑣 ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) ) }
31		df-opab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) ) }
32		df-opab	⊢ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) } = { 𝑧 ∣ ∃ 𝑢 ∃ 𝑣 ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ ∧ ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) ) }
33	30 31 32	3sstr4i	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) } ⊆ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) }
34		df-xp	⊢ ( V × V ) = { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) }
35	33 34	sseqtrri	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) } ⊆ ( V × V )
36	6 35	sstri	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ ( V × V )
37	1 36	eqsstri	⊢ 𝐴 ⊆ ( V × V )
38		df-rel	⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )
39	37 38	mpbir	⊢ Rel 𝐴