Theorem relopabiv 5779

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 5781. (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 3446	. . . . . 6 ⊢ 𝑥 ∈ V
2		vex 3446	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	pm3.2i 470	. . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
5	4	ssopab2i 5508	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6		relopabiv.1	. . 3 ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
7		df-xp 5640	. . 3 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
8	5, 6, 7	3sstr4i 3987	. 2 ⊢ 𝐴 ⊆ (V × V)
9		df-rel 5641	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
10	8, 9	mpbir 231	1 ⊢ Rel 𝐴

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903  {copab 5162   × cxp 5632  Rel wrel 5639

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 3444  df-ss 3920  df-opab 5163  df-xp 5640  df-rel 5641

This theorem is referenced by:  relopabv  5780  mptrel  5784  reli  5785  rele  5786  relcnv  6073  relco  6077  brfvopabrbr  6948  reloprab  7429  reldmoprab  7477  relrpss  7681  eqer  8684  ecopover  8772  relen  8902  reldom  8903  relfsupp  9280  relwdom  9485  fpwwe2lem2  10557  fpwwe2lem3  10558  fpwwe2lem5  10560  fpwwe2lem6  10561  fpwwe2lem8  10563  fpwwe2lem10  10565  fpwwe2lem11  10566  fpwwe2lem12  10567  fpwwelem  10570  climrel  15429  rlimrel  15430  brstruct  17089  sscrel  17751  gaorber  19254  sylow2a  19565  efgrelexlemb  19696  efgcpbllemb  19701  rellindf  21780  psrbaglesupp  21895  2ndcctbss  23416  refrel  23469  vitalilem1  25582  lgsquadlem1  27364  lgsquadlem2  27365  dmcuts  27804  relsubgr  29360  vcrel  30654  h2hlm  31074  hlimi  31282  erler  33365  relfldext  33828  finextfldext  33848  relmntop  34208  relae  34424  fineqvnttrclse  35308  fnerel  36560  filnetlem3  36602  brabg2  37997  heiborlem3  38093  heiborlem4  38094  relrngo  38176  isdivrngo  38230  drngoi  38231  isdrngo1  38236  riscer  38268  relcoss  38793  relssr  38860  prter1  39284  prter3  39287  prjsper  42995  reldvds  44700  nelbrim  47664  rellininds  48832