Theorem relopabiv 5763

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3436   ⊆ wss 3903  {copab 5154   × cxp 5617  Rel wrel 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-opab 5155  df-xp 5625  df-rel 5626

This theorem is referenced by:  relopabv  5764  mptrel  5768  reli  5769  rele  5770  relcnv  6055  relco  6059  brfvopabrbr  6927  reloprab  7408  reldmoprab  7456  relrpss  7660  eqer  8661  ecopover  8748  relen  8877  reldom  8878  relfsupp  9253  relwdom  9458  fpwwe2lem2  10526  fpwwe2lem3  10527  fpwwe2lem5  10529  fpwwe2lem6  10530  fpwwe2lem8  10532  fpwwe2lem10  10534  fpwwe2lem11  10535  fpwwe2lem12  10536  fpwwelem  10539  climrel  15399  rlimrel  15400  brstruct  17059  sscrel  17720  gaorber  19187  sylow2a  19498  efgrelexlemb  19629  efgcpbllemb  19634  rellindf  21715  psrbaglesupp  21829  2ndcctbss  23340  refrel  23393  vitalilem1  25507  lgsquadlem1  27289  lgsquadlem2  27290  dmscut  27722  relsubgr  29214  vcrel  30504  h2hlm  30924  hlimi  31132  erler  33206  relfldext  33617  finextfldext  33637  relmntop  33997  relae  34213  fineqvnttrclse  35083  fnerel  36322  filnetlem3  36364  brabg2  37707  heiborlem3  37803  heiborlem4  37804  relrngo  37886  isdivrngo  37940  drngoi  37941  isdrngo1  37946  riscer  37978  relcoss  38410  relssr  38487  prter1  38868  prter3  38871  prjsper  42591  reldvds  44298  nelbrim  47269  rellininds  48438