Theorem relopabiv 5832

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

Syntax hints:   ∧ wa 395   = wceq 1536   ∈ wcel 2105  Vcvv 3477   ⊆ wss 3962  {copab 5209   × cxp 5686  Rel wrel 5693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-opab 5210  df-xp 5694  df-rel 5695

This theorem is referenced by:  relopabv  5833  mptrel  5837  reli  5838  rele  5839  relcnv  6124  relco  6128  brfvopabrbr  7012  reloprab  7491  reldmoprab  7538  relrpss  7742  eqer  8779  ecopover  8859  relen  8988  reldom  8989  relfsupp  9400  relwdom  9603  fpwwe2lem2  10669  fpwwe2lem3  10670  fpwwe2lem5  10672  fpwwe2lem6  10673  fpwwe2lem8  10675  fpwwe2lem10  10677  fpwwe2lem11  10678  fpwwe2lem12  10679  fpwwelem  10682  climrel  15524  rlimrel  15525  brstruct  17181  sscrel  17860  gaorber  19338  sylow2a  19651  efgrelexlemb  19782  efgcpbllemb  19787  rellindf  21845  psrbaglesupp  21959  2ndcctbss  23478  refrel  23531  vitalilem1  25656  lgsquadlem1  27438  lgsquadlem2  27439  dmscut  27870  relsubgr  29300  vcrel  30588  h2hlm  31008  hlimi  31216  erler  33251  relfldext  33673  relmntop  33986  relae  34220  fnerel  36320  filnetlem3  36362  brabg2  37703  heiborlem3  37799  heiborlem4  37800  relrngo  37882  isdivrngo  37936  drngoi  37937  isdrngo1  37942  riscer  37974  relcoss  38404  relssr  38481  prter1  38860  prter3  38863  prjsper  42594  reldvds  44310  nelbrim  47224  rellininds  48288