Theorem relopabiv 5768

Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but a longer proof using ax-11 2163 and ax-12 2183, see relopabi 5770. (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 3443	. . . . . 6 ⊢ 𝑥 ∈ V
2		vex 3443	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	pm3.2i 470	. . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
5	4	ssopab2i 5497	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6		relopabiv.1	. . 3 ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
7		df-xp 5629	. . 3 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
8	5, 6, 7	3sstr4i 3984	. 2 ⊢ 𝐴 ⊆ (V × V)
9		df-rel 5630	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
10	8, 9	mpbir 231	1 ⊢ Rel 𝐴

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3439   ⊆ wss 3900  {copab 5159   × cxp 5621  Rel wrel 5628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3441  df-ss 3917  df-opab 5160  df-xp 5629  df-rel 5630

This theorem is referenced by:  relopabv  5769  mptrel  5773  reli  5774  rele  5775  relcnv  6062  relco  6066  brfvopabrbr  6937  reloprab  7417  reldmoprab  7465  relrpss  7669  eqer  8672  ecopover  8760  relen  8890  reldom  8891  relfsupp  9268  relwdom  9473  fpwwe2lem2  10545  fpwwe2lem3  10546  fpwwe2lem5  10548  fpwwe2lem6  10549  fpwwe2lem8  10551  fpwwe2lem10  10553  fpwwe2lem11  10554  fpwwe2lem12  10555  fpwwelem  10558  climrel  15417  rlimrel  15418  brstruct  17077  sscrel  17739  gaorber  19239  sylow2a  19550  efgrelexlemb  19681  efgcpbllemb  19686  rellindf  21765  psrbaglesupp  21880  2ndcctbss  23401  refrel  23454  vitalilem1  25567  lgsquadlem1  27349  lgsquadlem2  27350  dmscut  27787  relsubgr  29323  vcrel  30616  h2hlm  31036  hlimi  31244  erler  33326  relfldext  33780  finextfldext  33800  relmntop  34160  relae  34376  fineqvnttrclse  35259  fnerel  36511  filnetlem3  36553  brabg2  37887  heiborlem3  37983  heiborlem4  37984  relrngo  38066  isdivrngo  38120  drngoi  38121  isdrngo1  38126  riscer  38158  relcoss  38683  relssr  38750  prter1  39174  prter3  39177  prjsper  42888  reldvds  44593  nelbrim  47558  rellininds  48726