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

Theorem relopabiv 5830
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 5832. (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 3484 . . . . . 6 𝑥 ∈ V
2 vex 3484 . . . . . 6 𝑦 ∈ V
31, 2pm3.2i 470 . . . . 5 (𝑥 ∈ V ∧ 𝑦 ∈ V)
43a1i 11 . . . 4 (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
54ssopab2i 5555 . . 3 {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6 relopabiv.1 . . 3 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
7 df-xp 5691 . . 3 (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
85, 6, 73sstr4i 4035 . 2 𝐴 ⊆ (V × V)
9 df-rel 5692 . 2 (Rel 𝐴𝐴 ⊆ (V × V))
108, 9mpbir 231 1 Rel 𝐴
Colors of variables: wff setvar class
Syntax hints:  wa 395   = wceq 1540  wcel 2108  Vcvv 3480  wss 3951  {copab 5205   × cxp 5683  Rel wrel 5690
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 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-opab 5206  df-xp 5691  df-rel 5692
This theorem is referenced by:  relopabv  5831  mptrel  5835  reli  5836  rele  5837  relcnv  6122  relco  6126  brfvopabrbr  7013  reloprab  7492  reldmoprab  7540  relrpss  7744  eqer  8781  ecopover  8861  relen  8990  reldom  8991  relfsupp  9403  relwdom  9606  fpwwe2lem2  10672  fpwwe2lem3  10673  fpwwe2lem5  10675  fpwwe2lem6  10676  fpwwe2lem8  10678  fpwwe2lem10  10680  fpwwe2lem11  10681  fpwwe2lem12  10682  fpwwelem  10685  climrel  15528  rlimrel  15529  brstruct  17185  sscrel  17857  gaorber  19326  sylow2a  19637  efgrelexlemb  19768  efgcpbllemb  19773  rellindf  21828  psrbaglesupp  21942  2ndcctbss  23463  refrel  23516  vitalilem1  25643  lgsquadlem1  27424  lgsquadlem2  27425  dmscut  27856  relsubgr  29286  vcrel  30579  h2hlm  30999  hlimi  31207  erler  33269  relfldext  33697  relmntop  34025  relae  34241  fnerel  36339  filnetlem3  36381  brabg2  37724  heiborlem3  37820  heiborlem4  37821  relrngo  37903  isdivrngo  37957  drngoi  37958  isdrngo1  37963  riscer  37995  relcoss  38424  relssr  38501  prter1  38880  prter3  38883  prjsper  42618  reldvds  44334  nelbrim  47287  rellininds  48360
  Copyright terms: Public domain W3C validator