Theorem relopabiv 5803

Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but a longer proof using ax-11 2197 and ax-12 2216, see relopabi 5805. (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 3458	. . . . . 6 ⊢ 𝑥 ∈ V
2		vex 3458	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	pm3.2i 476	. . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
5	4	ssopab2i 5529	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6		relopabiv.1	. . 3 ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
7		df-xp 5661	. . 3 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
8	5, 6, 7	3sstr4i 3964	. 2 ⊢ 𝐴 ⊆ (V × V)
9		df-rel 5662	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
10	8, 9	mpbir 234	1 ⊢ Rel 𝐴

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900  {copab 5170   × cxp 5653  Rel wrel 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-opab 5171  df-xp 5661  df-rel 5662

This theorem is used by:  relopabv  5804  mptrel  5808  reli  5809  rele  5810  relcnv  6111  relco  6115  brfvopabrbr  7010  reloprab  7499  reldmoprab  7547  relrpss  7761  eqer  8779  ecopover  8867  relen  9003  reldom  9004  relfsupp  9380  relwdom  9584  fpwwe2lem2  10741  fpwwe2lem3  10742  fpwwe2lem5  10744  fpwwe2lem6  10745  fpwwe2lem8  10747  fpwwe2lem10  10749  fpwwe2lem11  10750  fpwwe2lem12  10751  fpwwelem  10754  climrel  15685  rlimrel  15686  brstruct  17352  sscrel  18014  gaorber  19549  sylow2a  19860  efgrelexlemb  19991  efgcpbllemb  19996  rellindf  22141  psrbaglesupp  22257  2ndcctbss  23801  refrel  23854  vitalilem1  25956  lgsquadlem1  27734  lgsquadlem2  27735  dmcuts  28204  relsubgr  29877  vcrel  31189  h2hlm  31609  hlimi  31817  erler  33893  relfldext  34343  finextfldext  34363  relmntop  34723  relae  34940  fineqvnttrclse  35891  fnerel  37303  filnetlem3  37345  brabg2  38842  heiborlem3  38938  heiborlem4  38939  relrngo  39021  isdivrngo  39075  drngoi  39076  isdrngo1  39081  riscer  39113  relcoss  39636  relssr  39703  prter1  40127  prter3  40130  prjsper  43827  reldvds  45489  nelbrim  48548  rellininds  49758