Theorem relopabiv 5679

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

Syntax hints:   ∧ wa 399   = wceq 1543   ∈ wcel 2110  Vcvv 3401   ⊆ wss 3857  {copab 5105   × cxp 5538  Rel wrel 5545

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 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2706

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2713  df-cleq 2726  df-clel 2812  df-v 3403  df-in 3864  df-ss 3874  df-opab 5106  df-xp 5546  df-rel 5547

This theorem is referenced by:  relopabv  5680  mptrel  5684  reli  5685  rele  5686  relcnv  5961  cotrg  5965  relco  6097  brfvopabrbr  6804  reloprab  7259  reldmoprab  7305  relrpss  7501  eqer  8415  ecopover  8492  relen  8620  reldom  8621  relfsupp  8976  relwdom  9171  fpwwe2lem2  10229  fpwwe2lem3  10230  fpwwe2lem5  10232  fpwwe2lem6  10233  fpwwe2lem8  10235  fpwwe2lem10  10237  fpwwe2lem11  10238  fpwwe2lem12  10239  fpwwelem  10242  climrel  15036  rlimrel  15037  brstruct  16693  sscrel  17290  gaorber  18674  sylow2a  18980  efgrelexlemb  19112  efgcpbllemb  19117  rellindf  20742  psrbaglesupp  20855  2ndcctbss  22324  refrel  22377  vitalilem1  24477  lgsquadlem1  26233  lgsquadlem2  26234  relsubgr  27329  vcrel  28613  h2hlm  29033  hlimi  29241  relfldext  31407  relmntop  31658  relae  31892  dmscut  33699  fnerel  34221  filnetlem3  34263  brabg2  35568  heiborlem3  35665  heiborlem4  35666  relrngo  35748  isdivrngo  35802  drngoi  35803  isdrngo1  35808  riscer  35840  relcoss  36240  relssr  36312  prter1  36587  prter3  36590  prjsper  40107  reldvds  41558  nelbrim  44393  isomgrrel  44901  rellininds  45411