Theorem relopabiv 5783

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3447   ⊆ wss 3914  {copab 5169   × cxp 5636  Rel wrel 5643

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-opab 5170  df-xp 5644  df-rel 5645

This theorem is referenced by:  relopabv  5784  mptrel  5788  reli  5789  rele  5790  relcnv  6075  relco  6079  brfvopabrbr  6965  reloprab  7448  reldmoprab  7496  relrpss  7700  eqer  8707  ecopover  8794  relen  8923  reldom  8924  relfsupp  9314  relwdom  9519  fpwwe2lem2  10585  fpwwe2lem3  10586  fpwwe2lem5  10588  fpwwe2lem6  10589  fpwwe2lem8  10591  fpwwe2lem10  10593  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwelem  10598  climrel  15458  rlimrel  15459  brstruct  17118  sscrel  17775  gaorber  19240  sylow2a  19549  efgrelexlemb  19680  efgcpbllemb  19685  rellindf  21717  psrbaglesupp  21831  2ndcctbss  23342  refrel  23395  vitalilem1  25509  lgsquadlem1  27291  lgsquadlem2  27292  dmscut  27723  relsubgr  29196  vcrel  30489  h2hlm  30909  hlimi  31117  erler  33216  relfldext  33640  relmntop  34014  relae  34230  fnerel  36326  filnetlem3  36368  brabg2  37711  heiborlem3  37807  heiborlem4  37808  relrngo  37890  isdivrngo  37944  drngoi  37945  isdrngo1  37950  riscer  37982  relcoss  38414  relssr  38491  prter1  38872  prter3  38875  prjsper  42596  reldvds  44304  nelbrim  47276  rellininds  48432