Theorem relopabiv 5795

Description: A class of ordered pairs is a relation. For a version without a disjoint variable condition, but a longer proof using ax-11 2193 and ax-12 2214, see relopabi 5797. (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 3460	. . . . . 6 ⊢ 𝑥 ∈ V
2		vex 3460	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	pm3.2i 474	. . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
5	4	ssopab2i 5523	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6		relopabiv.1	. . 3 ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
7		df-xp 5655	. . 3 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
8	5, 6, 7	3sstr4i 3989	. 2 ⊢ 𝐴 ⊆ (V × V)
9		df-rel 5656	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
10	8, 9	mpbir 233	1 ⊢ Rel 𝐴

Syntax hints:   ∧ wa 399   = wceq 1562   ∈ wcel 2144  Vcvv 3456   ⊆ wss 3906  {copab 5164   × cxp 5647  Rel wrel 5654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-ss 3923  df-opab 5165  df-xp 5655  df-rel 5656

This theorem is referenced by:  relopabv  5796  mptrel  5800  reli  5801  rele  5802  relcnv  6095  relco  6099  brfvopabrbr  6974  reloprab  7457  reldmoprab  7505  relrpss  7709  eqer  8717  ecopover  8805  relen  8934  reldom  8935  relfsupp  9311  relwdom  9516  fpwwe2lem2  10592  fpwwe2lem3  10593  fpwwe2lem5  10595  fpwwe2lem6  10596  fpwwe2lem8  10598  fpwwe2lem10  10600  fpwwe2lem11  10601  fpwwe2lem12  10602  fpwwelem  10605  climrel  15521  rlimrel  15522  brstruct  17186  sscrel  17848  gaorber  19350  sylow2a  19661  efgrelexlemb  19792  efgcpbllemb  19797  rellindf  21862  psrbaglesupp  21976  2ndcctbss  23517  refrel  23570  vitalilem1  25672  lgsquadlem1  27446  lgsquadlem2  27447  dmcuts  27886  relsubgr  29472  vcrel  30765  h2hlm  31185  hlimi  31393  erler  33448  relfldext  33943  finextfldext  33963  relmntop  34323  relae  34539  fineqvnttrclse  35424  fnerel  36703  filnetlem3  36745  brabg2  38221  heiborlem3  38317  heiborlem4  38318  relrngo  38400  isdivrngo  38454  drngoi  38455  isdrngo1  38460  riscer  38492  relcoss  39017  relssr  39084  prter1  39508  prter3  39511  prjsper  43195  reldvds  44896  nelbrim  47874  rellininds  49070