Theorem relopabiv 5766

Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but a longer proof using ax-11 2170 and ax-12 2191, see relopabi 5768. (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 472	. . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
5	4	ssopab2i 5495	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6		relopabiv.1	. . 3 ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
7		df-xp 5627	. . 3 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
8	5, 6, 7	3sstr4i 3968	. 2 ⊢ 𝐴 ⊆ (V × V)
9		df-rel 5628	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
10	8, 9	mpbir 233	1 ⊢ Rel 𝐴

Syntax hints:   ∧ wa 397   = wceq 1548   ∈ wcel 2121  Vcvv 3433   ⊆ wss 3885  {copab 5137   × cxp 5619  Rel wrel 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3902  df-opab 5138  df-xp 5627  df-rel 5628

This theorem is referenced by:  relopabv  5767  mptrel  5771  reli  5772  rele  5773  relcnv  6063  relco  6067  brfvopabrbr  6936  reloprab  7419  reldmoprab  7467  relrpss  7671  eqer  8674  ecopover  8762  relen  8892  reldom  8893  relfsupp  9270  relwdom  9475  fpwwe2lem2  10550  fpwwe2lem3  10551  fpwwe2lem5  10553  fpwwe2lem6  10554  fpwwe2lem8  10556  fpwwe2lem10  10558  fpwwe2lem11  10559  fpwwe2lem12  10560  fpwwelem  10563  climrel  15449  rlimrel  15450  brstruct  17113  sscrel  17775  gaorber  19278  sylow2a  19589  efgrelexlemb  19720  efgcpbllemb  19725  rellindf  21787  psrbaglesupp  21901  2ndcctbss  23442  refrel  23495  vitalilem1  25597  lgsquadlem1  27365  lgsquadlem2  27366  dmcuts  27805  relsubgr  29360  vcrel  30653  h2hlm  31073  hlimi  31281  erler  33350  relfldext  33840  finextfldext  33860  relmntop  34220  relae  34436  fineqvnttrclse  35320  fnerel  36581  filnetlem3  36623  brabg2  38099  heiborlem3  38195  heiborlem4  38196  relrngo  38278  isdivrngo  38332  drngoi  38333  isdrngo1  38338  riscer  38370  relcoss  38895  relssr  38962  prter1  39386  prter3  39389  prjsper  43073  reldvds  44774  nelbrim  47752  rellininds  48948