Theorem relopabiv 5770

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3441   ⊆ wss 3902  {copab 5161   × cxp 5623  Rel wrel 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-ss 3919  df-opab 5162  df-xp 5631  df-rel 5632

This theorem is referenced by:  relopabv  5771  mptrel  5775  reli  5776  rele  5777  relcnv  6064  relco  6068  brfvopabrbr  6939  reloprab  7419  reldmoprab  7467  relrpss  7671  eqer  8674  ecopover  8762  relen  8892  reldom  8893  relfsupp  9270  relwdom  9475  fpwwe2lem2  10547  fpwwe2lem3  10548  fpwwe2lem5  10550  fpwwe2lem6  10551  fpwwe2lem8  10553  fpwwe2lem10  10555  fpwwe2lem11  10556  fpwwe2lem12  10557  fpwwelem  10560  climrel  15419  rlimrel  15420  brstruct  17079  sscrel  17741  gaorber  19241  sylow2a  19552  efgrelexlemb  19683  efgcpbllemb  19688  rellindf  21767  psrbaglesupp  21882  2ndcctbss  23403  refrel  23456  vitalilem1  25569  lgsquadlem1  27351  lgsquadlem2  27352  dmcuts  27791  relsubgr  29346  vcrel  30639  h2hlm  31059  hlimi  31267  erler  33349  relfldext  33803  finextfldext  33823  relmntop  34183  relae  34399  fineqvnttrclse  35282  fnerel  36534  filnetlem3  36576  brabg2  37920  heiborlem3  38016  heiborlem4  38017  relrngo  38099  isdivrngo  38153  drngoi  38154  isdrngo1  38159  riscer  38191  relcoss  38716  relssr  38783  prter1  39207  prter3  39210  prjsper  42918  reldvds  44623  nelbrim  47588  rellininds  48756