Theorem relopabiv 5806

Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but a longer proof using ax-11 2191 and ax-12 2212, see relopabi 5808. (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 3458	. . . . . 6 ⊢ 𝑥 ∈ V
2		vex 3458	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	pm3.2i 475	. . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
5	4	ssopab2i 5534	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6		relopabiv.1	. . 3 ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
7		df-xp 5666	. . 3 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
8	5, 6, 7	3sstr4i 3987	. 2 ⊢ 𝐴 ⊆ (V × V)
9		df-rel 5667	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
10	8, 9	mpbir 234	1 ⊢ Rel 𝐴

This proof depends on syntax axioms:   ∧ wa 400   = wceq 1569   ∈ wcel 2142  Vcvv 3454   ⊆ wss 3904  {copab 5172   × cxp 5658  Rel wrel 5665

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-opab 5173  df-xp 5666  df-rel 5667

This theorem is used by:  relopabv  5807  mptrel  5811  reli  5812  rele  5813  relcnv  6105  relco  6109  brfvopabrbr  6986  reloprab  7471  reldmoprab  7519  relrpss  7723  eqer  8729  ecopover  8817  relen  8946  reldom  8947  relfsupp  9321  relwdom  9526  fpwwe2lem2  10623  fpwwe2lem3  10624  fpwwe2lem5  10626  fpwwe2lem6  10627  fpwwe2lem8  10629  fpwwe2lem10  10631  fpwwe2lem11  10632  fpwwe2lem12  10633  fpwwelem  10636  climrel  15550  rlimrel  15551  brstruct  17214  sscrel  17876  gaorber  19384  sylow2a  19695  efgrelexlemb  19826  efgcpbllemb  19831  rellindf  21969  psrbaglesupp  22083  2ndcctbss  23623  refrel  23676  vitalilem1  25778  lgsquadlem1  27555  lgsquadlem2  27556  dmcuts  27995  relsubgr  29630  vcrel  30923  h2hlm  31343  hlimi  31551  erler  33594  relfldext  34043  finextfldext  34063  relmntop  34423  relae  34639  fineqvnttrclse  35545  fnerel  36877  filnetlem3  36919  brabg2  38396  heiborlem3  38492  heiborlem4  38493  relrngo  38575  isdivrngo  38629  drngoi  38630  isdrngo1  38635  riscer  38667  relcoss  39190  relssr  39257  prter1  39681  prter3  39684  prjsper  43368  reldvds  45053  nelbrim  48040  rellininds  49251