Theorem relopabiv 5797

Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but a longer proof using ax-11 2193 and ax-12 2212, see relopabi 5799. (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 3454	. . . . . 6 ⊢ 𝑥 ∈ V
2		vex 3454	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	pm3.2i 476	. . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
5	4	ssopab2i 5524	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6		relopabiv.1	. . 3 ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
7		df-xp 5656	. . 3 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
8	5, 6, 7	3sstr4i 3959	. 2 ⊢ 𝐴 ⊆ (V × V)
9		df-rel 5657	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
10	8, 9	mpbir 234	1 ⊢ Rel 𝐴

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895  {copab 5166   × cxp 5648  Rel wrel 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-opab 5167  df-xp 5656  df-rel 5657

This theorem is used by:  relopabv  5798  mptrel  5802  reli  5803  rele  5804  relcnv  6099  relco  6103  brfvopabrbr  6990  reloprab  7479  reldmoprab  7527  relrpss  7740  eqer  8754  ecopover  8842  relen  8978  reldom  8979  relfsupp  9355  relwdom  9560  fpwwe2lem2  10717  fpwwe2lem3  10718  fpwwe2lem5  10720  fpwwe2lem6  10721  fpwwe2lem8  10723  fpwwe2lem10  10725  fpwwe2lem11  10726  fpwwe2lem12  10727  fpwwelem  10730  climrel  15659  rlimrel  15660  brstruct  17326  sscrel  17988  gaorber  19522  sylow2a  19833  efgrelexlemb  19964  efgcpbllemb  19969  rellindf  22114  psrbaglesupp  22230  2ndcctbss  23774  refrel  23827  vitalilem1  25929  lgsquadlem1  27707  lgsquadlem2  27708  dmcuts  28177  relsubgr  29850  vcrel  31162  h2hlm  31582  hlimi  31790  erler  33826  relfldext  34276  finextfldext  34296  relmntop  34656  relae  34873  fineqvnttrclse  35792  fnerel  37126  filnetlem3  37168  brabg2  38652  heiborlem3  38748  heiborlem4  38749  relrngo  38831  isdivrngo  38885  drngoi  38886  isdrngo1  38891  riscer  38923  relcoss  39446  relssr  39513  prter1  39937  prter3  39940  prjsper  43637  reldvds  45299  nelbrim  48345  rellininds  49555