Theorem relopabiv 5774

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3444   ⊆ wss 3911  {copab 5164   × cxp 5629  Rel wrel 5636

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 3446  df-ss 3928  df-opab 5165  df-xp 5637  df-rel 5638

This theorem is referenced by:  relopabv  5775  mptrel  5779  reli  5780  rele  5781  relcnv  6064  relco  6068  brfvopabrbr  6947  reloprab  7428  reldmoprab  7476  relrpss  7680  eqer  8684  ecopover  8771  relen  8900  reldom  8901  relfsupp  9290  relwdom  9495  fpwwe2lem2  10561  fpwwe2lem3  10562  fpwwe2lem5  10564  fpwwe2lem6  10565  fpwwe2lem8  10567  fpwwe2lem10  10569  fpwwe2lem11  10570  fpwwe2lem12  10571  fpwwelem  10574  climrel  15434  rlimrel  15435  brstruct  17094  sscrel  17755  gaorber  19222  sylow2a  19533  efgrelexlemb  19664  efgcpbllemb  19669  rellindf  21750  psrbaglesupp  21864  2ndcctbss  23375  refrel  23428  vitalilem1  25542  lgsquadlem1  27324  lgsquadlem2  27325  dmscut  27757  relsubgr  29249  vcrel  30539  h2hlm  30959  hlimi  31167  erler  33232  relfldext  33633  relmntop  34007  relae  34223  fnerel  36319  filnetlem3  36361  brabg2  37704  heiborlem3  37800  heiborlem4  37801  relrngo  37883  isdivrngo  37937  drngoi  37938  isdrngo1  37943  riscer  37975  relcoss  38407  relssr  38484  prter1  38865  prter3  38868  prjsper  42589  reldvds  44297  nelbrim  47269  rellininds  48425