MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  relopabiv Structured version   Visualization version   GIF version

Theorem relopabiv 5781
Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but a longer proof using ax-11 2155 and ax-12 2172, see relopabi 5783. (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
StepHypRef Expression
1 vex 3452 . . . . . 6 𝑥 ∈ V
2 vex 3452 . . . . . 6 𝑦 ∈ V
31, 2pm3.2i 472 . . . . 5 (𝑥 ∈ V ∧ 𝑦 ∈ V)
43a1i 11 . . . 4 (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
54ssopab2i 5512 . . 3 {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6 relopabiv.1 . . 3 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
7 df-xp 5644 . . 3 (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
85, 6, 73sstr4i 3992 . 2 𝐴 ⊆ (V × V)
9 df-rel 5645 . 2 (Rel 𝐴𝐴 ⊆ (V × V))
108, 9mpbir 230 1 Rel 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 397   = wceq 1542  wcel 2107  Vcvv 3448  wss 3915  {copab 5172   × 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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932  df-opab 5173  df-xp 5644  df-rel 5645
This theorem is referenced by:  relopabv  5782  mptrel  5786  reli  5787  rele  5788  relcnv  6061  relco  6065  brfvopabrbr  6950  reloprab  7421  reldmoprab  7467  relrpss  7666  eqer  8690  ecopover  8767  relen  8895  reldom  8896  relfsupp  9314  relwdom  9509  fpwwe2lem2  10575  fpwwe2lem3  10576  fpwwe2lem5  10578  fpwwe2lem6  10579  fpwwe2lem8  10581  fpwwe2lem10  10583  fpwwe2lem11  10584  fpwwe2lem12  10585  fpwwelem  10588  climrel  15381  rlimrel  15382  brstruct  17027  sscrel  17703  gaorber  19095  sylow2a  19408  efgrelexlemb  19539  efgcpbllemb  19544  rellindf  21230  psrbaglesupp  21342  2ndcctbss  22822  refrel  22875  vitalilem1  24988  lgsquadlem1  26744  lgsquadlem2  26745  dmscut  27172  relsubgr  28259  vcrel  29544  h2hlm  29964  hlimi  30172  relfldext  32375  relmntop  32645  relae  32879  fnerel  34839  filnetlem3  34881  brabg2  36204  heiborlem3  36301  heiborlem4  36302  relrngo  36384  isdivrngo  36438  drngoi  36439  isdrngo1  36444  riscer  36476  relcoss  36914  relssr  36991  prter1  37370  prter3  37373  prjsper  40975  reldvds  42669  nelbrim  45581  isomgrrel  46088  rellininds  46598
  Copyright terms: Public domain W3C validator