Theorem relopabiv 5771

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 2185, see relopabi 5773. (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 3434	. . . . . 6 ⊢ 𝑥 ∈ V
2		vex 3434	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	pm3.2i 470	. . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
5	4	ssopab2i 5500	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6		relopabiv.1	. . 3 ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
7		df-xp 5632	. . 3 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
8	5, 6, 7	3sstr4i 3974	. 2 ⊢ 𝐴 ⊆ (V × V)
9		df-rel 5633	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
10	8, 9	mpbir 231	1 ⊢ Rel 𝐴

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890  {copab 5148   × cxp 5624  Rel wrel 5631

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-opab 5149  df-xp 5632  df-rel 5633

This theorem is referenced by:  relopabv  5772  mptrel  5776  reli  5777  rele  5778  relcnv  6065  relco  6069  brfvopabrbr  6940  reloprab  7421  reldmoprab  7469  relrpss  7673  eqer  8675  ecopover  8763  relen  8893  reldom  8894  relfsupp  9271  relwdom  9476  fpwwe2lem2  10550  fpwwe2lem3  10551  fpwwe2lem5  10553  fpwwe2lem6  10554  fpwwe2lem8  10556  fpwwe2lem10  10558  fpwwe2lem11  10559  fpwwe2lem12  10560  fpwwelem  10563  climrel  15449  rlimrel  15450  brstruct  17113  sscrel  17775  gaorber  19278  sylow2a  19589  efgrelexlemb  19720  efgcpbllemb  19725  rellindf  21802  psrbaglesupp  21916  2ndcctbss  23434  refrel  23487  vitalilem1  25589  lgsquadlem1  27361  lgsquadlem2  27362  dmcuts  27801  relsubgr  29356  vcrel  30650  h2hlm  31070  hlimi  31278  erler  33345  relfldext  33808  finextfldext  33828  relmntop  34188  relae  34404  fineqvnttrclse  35288  fnerel  36540  filnetlem3  36582  brabg2  38058  heiborlem3  38154  heiborlem4  38155  relrngo  38237  isdivrngo  38291  drngoi  38292  isdrngo1  38297  riscer  38329  relcoss  38854  relssr  38921  prter1  39345  prter3  39348  prjsper  43061  reldvds  44766  nelbrim  47741  rellininds  48937