Theorem relopabiv 5794

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3450   ⊆ wss 3898  {copab 5166   × cxp 5645  Rel wrel 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3915  df-opab 5167  df-xp 5653  df-rel 5654

This theorem is used by:  relopabv  5795  mptrel  5799  reli  5800  rele  5801  relcnv  6094  relco  6098  brfvopabrbr  6978  reloprab  7467  reldmoprab  7515  relrpss  7723  eqer  8732  ecopover  8820  relen  8956  reldom  8957  relfsupp  9333  relwdom  9538  fpwwe2lem2  10688  fpwwe2lem3  10689  fpwwe2lem5  10691  fpwwe2lem6  10692  fpwwe2lem8  10694  fpwwe2lem10  10696  fpwwe2lem11  10697  fpwwe2lem12  10698  fpwwelem  10701  climrel  15626  rlimrel  15627  brstruct  17287  sscrel  17949  gaorber  19483  sylow2a  19794  efgrelexlemb  19925  efgcpbllemb  19930  rellindf  22075  psrbaglesupp  22191  2ndcctbss  23735  refrel  23788  vitalilem1  25890  lgsquadlem1  27670  lgsquadlem2  27671  dmcuts  28110  relsubgr  29783  vcrel  31095  h2hlm  31515  hlimi  31723  erler  33759  relfldext  34209  finextfldext  34229  relmntop  34589  relae  34806  fineqvnttrclse  35717  fnerel  37048  filnetlem3  37090  brabg2  38571  heiborlem3  38667  heiborlem4  38668  relrngo  38750  isdivrngo  38804  drngoi  38805  isdrngo1  38810  riscer  38842  relcoss  39365  relssr  39432  prter1  39856  prter3  39859  prjsper  43558  reldvds  45243  nelbrim  48267  rellininds  49477