Theorem relopabiv 5808

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

Syntax hints:   ∧ wa 400   = wceq 1567   ∈ wcel 2149  Vcvv 3461   ⊆ wss 3911  {copab 5175   × cxp 5660  Rel wrel 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3463  df-ss 3928  df-opab 5176  df-xp 5668  df-rel 5669

This theorem is referenced by:  relopabv  5809  mptrel  5813  reli  5814  rele  5815  relcnv  6107  relco  6111  brfvopabrbr  6987  reloprab  7470  reldmoprab  7518  relrpss  7722  eqer  8731  ecopover  8819  relen  8948  reldom  8949  relfsupp  9323  relwdom  9528  fpwwe2lem2  10617  fpwwe2lem3  10618  fpwwe2lem5  10620  fpwwe2lem6  10621  fpwwe2lem8  10623  fpwwe2lem10  10625  fpwwe2lem11  10626  fpwwe2lem12  10627  fpwwelem  10630  climrel  15543  rlimrel  15544  brstruct  17208  sscrel  17870  gaorber  19378  sylow2a  19689  efgrelexlemb  19820  efgcpbllemb  19825  rellindf  21927  psrbaglesupp  22041  2ndcctbss  23581  refrel  23634  vitalilem1  25736  lgsquadlem1  27510  lgsquadlem2  27511  dmcuts  27950  relsubgr  29560  vcrel  30853  h2hlm  31273  hlimi  31481  erler  33526  relfldext  33979  finextfldext  33999  relmntop  34359  relae  34575  fineqvnttrclse  35470  fnerel  36772  filnetlem3  36814  brabg2  38291  heiborlem3  38387  heiborlem4  38388  relrngo  38470  isdivrngo  38524  drngoi  38525  isdrngo1  38530  riscer  38562  relcoss  39087  relssr  39154  prter1  39578  prter3  39581  prjsper  43267  reldvds  44952  nelbrim  47936  rellininds  49143