Theorem relopabiv 5786

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 5788. (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 470	. . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
5	4	ssopab2i 5513	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6		relopabiv.1	. . 3 ⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}
7		df-xp 5647	. . 3 ⊢ (V × V) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
8	5, 6, 7	3sstr4i 4001	. 2 ⊢ 𝐴 ⊆ (V × V)
9		df-rel 5648	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
10	8, 9	mpbir 231	1 ⊢ Rel 𝐴

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3450   ⊆ wss 3917  {copab 5172   × cxp 5639  Rel wrel 5646

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-opab 5173  df-xp 5647  df-rel 5648

This theorem is referenced by:  relopabv  5787  mptrel  5791  reli  5792  rele  5793  relcnv  6078  relco  6082  brfvopabrbr  6968  reloprab  7451  reldmoprab  7499  relrpss  7703  eqer  8710  ecopover  8797  relen  8926  reldom  8927  relfsupp  9321  relwdom  9526  fpwwe2lem2  10592  fpwwe2lem3  10593  fpwwe2lem5  10595  fpwwe2lem6  10596  fpwwe2lem8  10598  fpwwe2lem10  10600  fpwwe2lem11  10601  fpwwe2lem12  10602  fpwwelem  10605  climrel  15465  rlimrel  15466  brstruct  17125  sscrel  17782  gaorber  19247  sylow2a  19556  efgrelexlemb  19687  efgcpbllemb  19692  rellindf  21724  psrbaglesupp  21838  2ndcctbss  23349  refrel  23402  vitalilem1  25516  lgsquadlem1  27298  lgsquadlem2  27299  dmscut  27730  relsubgr  29203  vcrel  30496  h2hlm  30916  hlimi  31124  erler  33223  relfldext  33647  relmntop  34021  relae  34237  fnerel  36333  filnetlem3  36375  brabg2  37718  heiborlem3  37814  heiborlem4  37815  relrngo  37897  isdivrngo  37951  drngoi  37952  isdrngo1  37957  riscer  37989  relcoss  38421  relssr  38498  prter1  38879  prter3  38882  prjsper  42603  reldvds  44311  nelbrim  47280  rellininds  48436