Theorem relopabiv 5799

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 5801. (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 3463	. . . . . 6 ⊢ 𝑥 ∈ V
2		vex 3463	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	pm3.2i 470	. . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
5	4	ssopab2i 5525	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6		relopabiv.1	. . 3 ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
7		df-xp 5660	. . 3 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
8	5, 6, 7	3sstr4i 4010	. 2 ⊢ 𝐴 ⊆ (V × V)
9		df-rel 5661	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
10	8, 9	mpbir 231	1 ⊢ Rel 𝐴

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Vcvv 3459   ⊆ wss 3926  {copab 5181   × cxp 5652  Rel wrel 5659

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-opab 5182  df-xp 5660  df-rel 5661

This theorem is referenced by:  relopabv  5800  mptrel  5804  reli  5805  rele  5806  relcnv  6091  relco  6095  brfvopabrbr  6983  reloprab  7466  reldmoprab  7514  relrpss  7718  eqer  8755  ecopover  8835  relen  8964  reldom  8965  relfsupp  9375  relwdom  9580  fpwwe2lem2  10646  fpwwe2lem3  10647  fpwwe2lem5  10649  fpwwe2lem6  10650  fpwwe2lem8  10652  fpwwe2lem10  10654  fpwwe2lem11  10655  fpwwe2lem12  10656  fpwwelem  10659  climrel  15508  rlimrel  15509  brstruct  17167  sscrel  17826  gaorber  19291  sylow2a  19600  efgrelexlemb  19731  efgcpbllemb  19736  rellindf  21768  psrbaglesupp  21882  2ndcctbss  23393  refrel  23446  vitalilem1  25561  lgsquadlem1  27343  lgsquadlem2  27344  dmscut  27775  relsubgr  29248  vcrel  30541  h2hlm  30961  hlimi  31169  erler  33260  relfldext  33686  relmntop  34055  relae  34271  fnerel  36356  filnetlem3  36398  brabg2  37741  heiborlem3  37837  heiborlem4  37838  relrngo  37920  isdivrngo  37974  drngoi  37975  isdrngo1  37980  riscer  38012  relcoss  38441  relssr  38518  prter1  38897  prter3  38900  prjsper  42631  reldvds  44339  nelbrim  47304  rellininds  48419