Theorem relopabiv 5719

Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but a longer proof using ax-11 2156 and ax-12 2173, see relopabi 5721. (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 3426	. . . . . 6 ⊢ 𝑥 ∈ V
2		vex 3426	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	pm3.2i 470	. . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
5	4	ssopab2i 5456	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6		relopabiv.1	. . 3 ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
7		df-xp 5586	. . 3 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
8	5, 6, 7	3sstr4i 3960	. 2 ⊢ 𝐴 ⊆ (V × V)
9		df-rel 5587	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
10	8, 9	mpbir 230	1 ⊢ Rel 𝐴

Syntax hints:   ∧ wa 395   = wceq 1539   ∈ wcel 2108  Vcvv 3422   ⊆ wss 3883  {copab 5132   × cxp 5578  Rel wrel 5585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-opab 5133  df-xp 5586  df-rel 5587

This theorem is referenced by:  relopabv  5720  mptrel  5724  reli  5725  rele  5726  relcnv  6001  cotrg  6005  relco  6137  brfvopabrbr  6854  reloprab  7312  reldmoprab  7358  relrpss  7555  eqer  8491  ecopover  8568  relen  8696  reldom  8697  relfsupp  9060  relwdom  9255  fpwwe2lem2  10319  fpwwe2lem3  10320  fpwwe2lem5  10322  fpwwe2lem6  10323  fpwwe2lem8  10325  fpwwe2lem10  10327  fpwwe2lem11  10328  fpwwe2lem12  10329  fpwwelem  10332  climrel  15129  rlimrel  15130  brstruct  16777  sscrel  17442  gaorber  18829  sylow2a  19139  efgrelexlemb  19271  efgcpbllemb  19276  rellindf  20925  psrbaglesupp  21037  2ndcctbss  22514  refrel  22567  vitalilem1  24677  lgsquadlem1  26433  lgsquadlem2  26434  relsubgr  27539  vcrel  28823  h2hlm  29243  hlimi  29451  relfldext  31623  relmntop  31874  relae  32108  dmscut  33932  fnerel  34454  filnetlem3  34496  brabg2  35801  heiborlem3  35898  heiborlem4  35899  relrngo  35981  isdivrngo  36035  drngoi  36036  isdrngo1  36041  riscer  36073  relcoss  36473  relssr  36545  prter1  36820  prter3  36823  prjsper  40368  reldvds  41822  nelbrim  44654  isomgrrel  45162  rellininds  45672