Theorem relopabiv 5805

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3453   ⊆ wss 3902  {copab 5171   × cxp 5657  Rel wrel 5664

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-opab 5172  df-xp 5665  df-rel 5666

This theorem is used by:  relopabv  5806  mptrel  5810  reli  5811  rele  5812  relcnv  6104  relco  6108  brfvopabrbr  6987  reloprab  7475  reldmoprab  7523  relrpss  7728  eqer  8736  ecopover  8824  relen  8960  reldom  8961  relfsupp  9336  relwdom  9541  fpwwe2lem2  10644  fpwwe2lem3  10645  fpwwe2lem5  10647  fpwwe2lem6  10648  fpwwe2lem8  10650  fpwwe2lem10  10652  fpwwe2lem11  10653  fpwwe2lem12  10654  fpwwelem  10657  climrel  15581  rlimrel  15582  brstruct  17244  sscrel  17906  gaorber  19436  sylow2a  19747  efgrelexlemb  19878  efgcpbllemb  19883  rellindf  22022  psrbaglesupp  22138  2ndcctbss  23682  refrel  23735  vitalilem1  25837  lgsquadlem1  27614  lgsquadlem2  27615  dmcuts  28054  relsubgr  29715  vcrel  31027  h2hlm  31447  hlimi  31655  erler  33692  relfldext  34141  finextfldext  34161  relmntop  34521  relae  34738  fineqvnttrclse  35637  fnerel  36944  filnetlem3  36986  brabg2  38454  heiborlem3  38550  heiborlem4  38551  relrngo  38633  isdivrngo  38687  drngoi  38688  isdrngo1  38693  riscer  38725  relcoss  39248  relssr  39315  prter1  39739  prter3  39742  prjsper  43441  reldvds  45126  nelbrim  48150  rellininds  49360