Theorem relopabiv 5747

Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but a longer proof using ax-11 2153 and ax-12 2170, see relopabi 5749. (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 3445	. . . . . 6 ⊢ 𝑥 ∈ V
2		vex 3445	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	pm3.2i 471	. . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
5	4	ssopab2i 5481	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6		relopabiv.1	. . 3 ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
7		df-xp 5611	. . 3 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
8	5, 6, 7	3sstr4i 3973	. 2 ⊢ 𝐴 ⊆ (V × V)
9		df-rel 5612	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
10	8, 9	mpbir 230	1 ⊢ Rel 𝐴

Syntax hints:   ∧ wa 396   = wceq 1540   ∈ wcel 2105  Vcvv 3441   ⊆ wss 3896  {copab 5147   × cxp 5603  Rel wrel 5610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3443  df-in 3903  df-ss 3913  df-opab 5148  df-xp 5611  df-rel 5612

This theorem is referenced by:  relopabv  5748  mptrel  5752  reli  5753  rele  5754  relcnv  6027  relco  6031  brfvopabrbr  6909  reloprab  7372  reldmoprab  7418  relrpss  7615  eqer  8579  ecopover  8656  relen  8784  reldom  8785  relfsupp  9198  relwdom  9393  fpwwe2lem2  10458  fpwwe2lem3  10459  fpwwe2lem5  10461  fpwwe2lem6  10462  fpwwe2lem8  10464  fpwwe2lem10  10466  fpwwe2lem11  10467  fpwwe2lem12  10468  fpwwelem  10471  climrel  15270  rlimrel  15271  brstruct  16916  sscrel  17592  gaorber  18981  sylow2a  19291  efgrelexlemb  19423  efgcpbllemb  19428  rellindf  21086  psrbaglesupp  21198  2ndcctbss  22677  refrel  22730  vitalilem1  24843  lgsquadlem1  26599  lgsquadlem2  26600  relsubgr  27744  vcrel  29030  h2hlm  29450  hlimi  29658  relfldext  31827  relmntop  32080  relae  32314  dmscut  34066  fnerel  34588  filnetlem3  34630  brabg2  35934  heiborlem3  36031  heiborlem4  36032  relrngo  36114  isdivrngo  36168  drngoi  36169  isdrngo1  36174  riscer  36206  relcoss  36649  relssr  36726  prter1  37105  prter3  37108  prjsper  40657  reldvds  42161  nelbrim  45026  isomgrrel  45533  rellininds  46043