Theorem relopabiv 5826

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

Syntax hints:   ∧ wa 394   = wceq 1534   ∈ wcel 2099  Vcvv 3462   ⊆ wss 3947  {copab 5215   × cxp 5680  Rel wrel 5687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-ss 3964  df-opab 5216  df-xp 5688  df-rel 5689

This theorem is referenced by:  relopabv  5827  mptrel  5831  reli  5832  rele  5833  relcnv  6114  relco  6118  brfvopabrbr  7006  reloprab  7484  reldmoprab  7531  relrpss  7735  eqer  8770  ecopover  8850  relen  8979  reldom  8980  relfsupp  9407  relwdom  9609  fpwwe2lem2  10675  fpwwe2lem3  10676  fpwwe2lem5  10678  fpwwe2lem6  10679  fpwwe2lem8  10681  fpwwe2lem10  10683  fpwwe2lem11  10684  fpwwe2lem12  10685  fpwwelem  10688  climrel  15494  rlimrel  15495  brstruct  17150  sscrel  17829  gaorber  19302  sylow2a  19617  efgrelexlemb  19748  efgcpbllemb  19753  rellindf  21806  psrbaglesupp  21921  2ndcctbss  23450  refrel  23503  vitalilem1  25628  lgsquadlem1  27409  lgsquadlem2  27410  dmscut  27841  relsubgr  29205  vcrel  30493  h2hlm  30913  hlimi  31121  erler  33120  relfldext  33535  relmntop  33839  relae  34073  fnerel  36050  filnetlem3  36092  brabg2  37418  heiborlem3  37514  heiborlem4  37515  relrngo  37597  isdivrngo  37651  drngoi  37652  isdrngo1  37657  riscer  37689  relcoss  38121  relssr  38198  prter1  38577  prter3  38580  prjsper  42262  reldvds  43989  nelbrim  46888  rellininds  47826