Theorem relopabiv 5830

Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but a longer proof using ax-11 2157 and ax-12 2177, see relopabi 5832. (Contributed by BJ, 22-Jul-2023.)

Hypothesis

Ref	Expression
relopabiv.1	⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Assertion

Ref	Expression
relopabiv	⊢ Rel 𝐴

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦)

Proof of Theorem relopabiv

Step	Hyp	Ref	Expression
1		vex 3484	. . . . . 6 ⊢ 𝑥 ∈ V
2		vex 3484	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	pm3.2i 470	. . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
5	4	ssopab2i 5555	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6		relopabiv.1	. . 3 ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
7		df-xp 5691	. . 3 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
8	5, 6, 7	3sstr4i 4035	. 2 ⊢ 𝐴 ⊆ (V × V)
9		df-rel 5692	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
10	8, 9	mpbir 231	1 ⊢ Rel 𝐴

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Vcvv 3480   ⊆ wss 3951  {copab 5205   × cxp 5683  Rel wrel 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-opab 5206  df-xp 5691  df-rel 5692

This theorem is referenced by:  relopabv  5831  mptrel  5835  reli  5836  rele  5837  relcnv  6122  relco  6126  brfvopabrbr  7013  reloprab  7492  reldmoprab  7540  relrpss  7744  eqer  8781  ecopover  8861  relen  8990  reldom  8991  relfsupp  9403  relwdom  9606  fpwwe2lem2  10672  fpwwe2lem3  10673  fpwwe2lem5  10675  fpwwe2lem6  10676  fpwwe2lem8  10678  fpwwe2lem10  10680  fpwwe2lem11  10681  fpwwe2lem12  10682  fpwwelem  10685  climrel  15528  rlimrel  15529  brstruct  17185  sscrel  17857  gaorber  19326  sylow2a  19637  efgrelexlemb  19768  efgcpbllemb  19773  rellindf  21828  psrbaglesupp  21942  2ndcctbss  23463  refrel  23516  vitalilem1  25643  lgsquadlem1  27424  lgsquadlem2  27425  dmscut  27856  relsubgr  29286  vcrel  30579  h2hlm  30999  hlimi  31207  erler  33269  relfldext  33697  relmntop  34025  relae  34241  fnerel  36339  filnetlem3  36381  brabg2  37724  heiborlem3  37820  heiborlem4  37821  relrngo  37903  isdivrngo  37957  drngoi  37958  isdrngo1  37963  riscer  37995  relcoss  38424  relssr  38501  prter1  38880  prter3  38883  prjsper  42618  reldvds  44334  nelbrim  47287  rellininds  48360