Theorem relopabiv 5759

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2111  Vcvv 3436   ⊆ wss 3897  {copab 5151   × cxp 5612  Rel wrel 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-opab 5152  df-xp 5620  df-rel 5621

This theorem is referenced by:  relopabv  5760  mptrel  5764  reli  5765  rele  5766  relcnv  6052  relco  6056  brfvopabrbr  6926  reloprab  7405  reldmoprab  7453  relrpss  7657  eqer  8658  ecopover  8745  relen  8874  reldom  8875  relfsupp  9247  relwdom  9452  fpwwe2lem2  10523  fpwwe2lem3  10524  fpwwe2lem5  10526  fpwwe2lem6  10527  fpwwe2lem8  10529  fpwwe2lem10  10531  fpwwe2lem11  10532  fpwwe2lem12  10533  fpwwelem  10536  climrel  15399  rlimrel  15400  brstruct  17059  sscrel  17720  gaorber  19220  sylow2a  19531  efgrelexlemb  19662  efgcpbllemb  19667  rellindf  21745  psrbaglesupp  21859  2ndcctbss  23370  refrel  23423  vitalilem1  25536  lgsquadlem1  27318  lgsquadlem2  27319  dmscut  27752  relsubgr  29247  vcrel  30540  h2hlm  30960  hlimi  31168  erler  33232  relfldext  33657  finextfldext  33677  relmntop  34037  relae  34253  fineqvnttrclse  35144  fnerel  36382  filnetlem3  36424  brabg2  37756  heiborlem3  37852  heiborlem4  37853  relrngo  37935  isdivrngo  37989  drngoi  37990  isdrngo1  37995  riscer  38027  relcoss  38524  relssr  38591  prter1  38977  prter3  38980  prjsper  42700  reldvds  44407  nelbrim  47374  rellininds  48543