Theorem relopabiv 5821

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

Syntax hints:   ∧ wa 397   = wceq 1542   ∈ wcel 2107  Vcvv 3475   ⊆ wss 3949  {copab 5211   × cxp 5675  Rel wrel 5682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-opab 5212  df-xp 5683  df-rel 5684

This theorem is referenced by:  relopabv  5822  mptrel  5826  reli  5827  rele  5828  relcnv  6104  relco  6108  brfvopabrbr  6996  reloprab  7468  reldmoprab  7514  relrpss  7714  eqer  8738  ecopover  8815  relen  8944  reldom  8945  relfsupp  9363  relwdom  9561  fpwwe2lem2  10627  fpwwe2lem3  10628  fpwwe2lem5  10630  fpwwe2lem6  10631  fpwwe2lem8  10633  fpwwe2lem10  10635  fpwwe2lem11  10636  fpwwe2lem12  10637  fpwwelem  10640  climrel  15436  rlimrel  15437  brstruct  17081  sscrel  17760  gaorber  19172  sylow2a  19487  efgrelexlemb  19618  efgcpbllemb  19623  rellindf  21363  psrbaglesupp  21477  2ndcctbss  22959  refrel  23012  vitalilem1  25125  lgsquadlem1  26883  lgsquadlem2  26884  dmscut  27312  relsubgr  28526  vcrel  29813  h2hlm  30233  hlimi  30441  relfldext  32725  relmntop  33004  relae  33238  fnerel  35223  filnetlem3  35265  brabg2  36585  heiborlem3  36681  heiborlem4  36682  relrngo  36764  isdivrngo  36818  drngoi  36819  isdrngo1  36824  riscer  36856  relcoss  37293  relssr  37370  prter1  37749  prter3  37752  prjsper  41350  reldvds  43074  nelbrim  45983  isomgrrel  46490  rellininds  47124