Theorem relopabiv 5844

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 5846. (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 3492	. . . . . 6 ⊢ 𝑥 ∈ V
2		vex 3492	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	pm3.2i 470	. . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
5	4	ssopab2i 5569	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6		relopabiv.1	. . 3 ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
7		df-xp 5706	. . 3 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
8	5, 6, 7	3sstr4i 4052	. 2 ⊢ 𝐴 ⊆ (V × V)
9		df-rel 5707	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
10	8, 9	mpbir 231	1 ⊢ Rel 𝐴

Syntax hints:   ∧ wa 395   = wceq 1537   ∈ wcel 2108  Vcvv 3488   ⊆ wss 3976  {copab 5228   × cxp 5698  Rel wrel 5705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-opab 5229  df-xp 5706  df-rel 5707

This theorem is referenced by:  relopabv  5845  mptrel  5849  reli  5850  rele  5851  relcnv  6134  relco  6138  brfvopabrbr  7026  reloprab  7509  reldmoprab  7556  relrpss  7759  eqer  8799  ecopover  8879  relen  9008  reldom  9009  relfsupp  9433  relwdom  9635  fpwwe2lem2  10701  fpwwe2lem3  10702  fpwwe2lem5  10704  fpwwe2lem6  10705  fpwwe2lem8  10707  fpwwe2lem10  10709  fpwwe2lem11  10710  fpwwe2lem12  10711  fpwwelem  10714  climrel  15538  rlimrel  15539  brstruct  17195  sscrel  17874  gaorber  19348  sylow2a  19661  efgrelexlemb  19792  efgcpbllemb  19797  rellindf  21851  psrbaglesupp  21965  2ndcctbss  23484  refrel  23537  vitalilem1  25662  lgsquadlem1  27442  lgsquadlem2  27443  dmscut  27874  relsubgr  29304  vcrel  30592  h2hlm  31012  hlimi  31220  erler  33237  relfldext  33659  relmntop  33970  relae  34204  fnerel  36304  filnetlem3  36346  brabg2  37677  heiborlem3  37773  heiborlem4  37774  relrngo  37856  isdivrngo  37910  drngoi  37911  isdrngo1  37916  riscer  37948  relcoss  38379  relssr  38456  prter1  38835  prter3  38838  prjsper  42563  reldvds  44284  nelbrim  47190  rellininds  48172