Theorem relopabiv 5791

Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but a longer proof using ax-11 2190 and ax-12 2211, see relopabi 5793. (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 3457	. . . . . 6 ⊢ 𝑥 ∈ V
2		vex 3457	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	pm3.2i 474	. . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
5	4	ssopab2i 5519	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6		relopabiv.1	. . 3 ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
7		df-xp 5651	. . 3 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
8	5, 6, 7	3sstr4i 3987	. 2 ⊢ 𝐴 ⊆ (V × V)
9		df-rel 5652	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
10	8, 9	mpbir 233	1 ⊢ Rel 𝐴

Syntax hints:   ∧ wa 399   = wceq 1559   ∈ wcel 2141  Vcvv 3453   ⊆ wss 3904  {copab 5161   × cxp 5643  Rel wrel 5650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3921  df-opab 5162  df-xp 5651  df-rel 5652

This theorem is referenced by:  relopabv  5792  mptrel  5796  reli  5797  rele  5798  relcnv  6088  relco  6092  brfvopabrbr  6966  reloprab  7449  reldmoprab  7497  relrpss  7701  eqer  8708  ecopover  8796  relen  8926  reldom  8927  relfsupp  9304  relwdom  9509  fpwwe2lem2  10585  fpwwe2lem3  10586  fpwwe2lem5  10588  fpwwe2lem6  10589  fpwwe2lem8  10591  fpwwe2lem10  10593  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwelem  10598  climrel  15500  rlimrel  15501  brstruct  17165  sscrel  17827  gaorber  19329  sylow2a  19640  efgrelexlemb  19771  efgcpbllemb  19776  rellindf  21838  psrbaglesupp  21952  2ndcctbss  23493  refrel  23546  vitalilem1  25648  lgsquadlem1  27419  lgsquadlem2  27420  dmcuts  27859  relsubgr  29414  vcrel  30707  h2hlm  31127  hlimi  31335  erler  33405  relfldext  33900  finextfldext  33920  relmntop  34280  relae  34496  fineqvnttrclse  35380  fnerel  36651  filnetlem3  36693  brabg2  38169  heiborlem3  38265  heiborlem4  38266  relrngo  38348  isdivrngo  38402  drngoi  38403  isdrngo1  38408  riscer  38440  relcoss  38965  relssr  39032  prter1  39456  prter3  39459  prjsper  43143  reldvds  44844  nelbrim  47822  rellininds  49018