Theorem relopabiv 5732

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 5734. (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 3437	. . . . . 6 ⊢ 𝑥 ∈ V
2		vex 3437	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	pm3.2i 471	. . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
5	4	ssopab2i 5464	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6		relopabiv.1	. . 3 ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
7		df-xp 5596	. . 3 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
8	5, 6, 7	3sstr4i 3965	. 2 ⊢ 𝐴 ⊆ (V × V)
9		df-rel 5597	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
10	8, 9	mpbir 230	1 ⊢ Rel 𝐴

Syntax hints:   ∧ wa 396   = wceq 1539   ∈ wcel 2107  Vcvv 3433   ⊆ wss 3888  {copab 5137   × cxp 5588  Rel wrel 5595

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-opab 5138  df-xp 5596  df-rel 5597

This theorem is referenced by:  relopabv  5733  mptrel  5737  reli  5738  rele  5739  relcnv  6015  relco  6019  brfvopabrbr  6881  reloprab  7343  reldmoprab  7389  relrpss  7586  eqer  8542  ecopover  8619  relen  8747  reldom  8748  relfsupp  9139  relwdom  9334  fpwwe2lem2  10397  fpwwe2lem3  10398  fpwwe2lem5  10400  fpwwe2lem6  10401  fpwwe2lem8  10403  fpwwe2lem10  10405  fpwwe2lem11  10406  fpwwe2lem12  10407  fpwwelem  10410  climrel  15210  rlimrel  15211  brstruct  16858  sscrel  17534  gaorber  18923  sylow2a  19233  efgrelexlemb  19365  efgcpbllemb  19370  rellindf  21024  psrbaglesupp  21136  2ndcctbss  22615  refrel  22668  vitalilem1  24781  lgsquadlem1  26537  lgsquadlem2  26538  relsubgr  27645  vcrel  28931  h2hlm  29351  hlimi  29559  relfldext  31730  relmntop  31983  relae  32217  dmscut  34014  fnerel  34536  filnetlem3  34578  brabg2  35883  heiborlem3  35980  heiborlem4  35981  relrngo  36063  isdivrngo  36117  drngoi  36118  isdrngo1  36123  riscer  36155  relcoss  36553  relssr  36625  prter1  36900  prter3  36903  prjsper  40454  reldvds  41940  nelbrim  44778  isomgrrel  45285  rellininds  45795