Theorem relopabiv 5820

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

Syntax hints:   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Vcvv 3474   ⊆ wss 3948  {copab 5210   × cxp 5674  Rel wrel 5681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-opab 5211  df-xp 5682  df-rel 5683

This theorem is referenced by:  relopabv  5821  mptrel  5825  reli  5826  rele  5827  relcnv  6103  relco  6107  brfvopabrbr  6995  reloprab  7470  reldmoprab  7516  relrpss  7716  eqer  8740  ecopover  8817  relen  8946  reldom  8947  relfsupp  9365  relwdom  9563  fpwwe2lem2  10629  fpwwe2lem3  10630  fpwwe2lem5  10632  fpwwe2lem6  10633  fpwwe2lem8  10635  fpwwe2lem10  10637  fpwwe2lem11  10638  fpwwe2lem12  10639  fpwwelem  10642  climrel  15438  rlimrel  15439  brstruct  17083  sscrel  17762  gaorber  19174  sylow2a  19489  efgrelexlemb  19620  efgcpbllemb  19625  rellindf  21369  psrbaglesupp  21483  2ndcctbss  22966  refrel  23019  vitalilem1  25132  lgsquadlem1  26890  lgsquadlem2  26891  dmscut  27320  relsubgr  28564  vcrel  29851  h2hlm  30271  hlimi  30479  relfldext  32784  relmntop  33073  relae  33307  fnerel  35309  filnetlem3  35351  brabg2  36671  heiborlem3  36767  heiborlem4  36768  relrngo  36850  isdivrngo  36904  drngoi  36905  isdrngo1  36910  riscer  36942  relcoss  37379  relssr  37456  prter1  37835  prter3  37838  prjsper  41432  reldvds  43156  nelbrim  46062  isomgrrel  46569  rellininds  47202