Theorem relopabiv 5776

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

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3429   ⊆ wss 3889  {copab 5147   × cxp 5629  Rel wrel 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-opab 5148  df-xp 5637  df-rel 5638

This theorem is referenced by:  relopabv  5777  mptrel  5781  reli  5782  rele  5783  relcnv  6069  relco  6073  brfvopabrbr  6944  reloprab  7426  reldmoprab  7474  relrpss  7678  eqer  8680  ecopover  8768  relen  8898  reldom  8899  relfsupp  9276  relwdom  9481  fpwwe2lem2  10555  fpwwe2lem3  10556  fpwwe2lem5  10558  fpwwe2lem6  10559  fpwwe2lem8  10561  fpwwe2lem10  10563  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwelem  10568  climrel  15454  rlimrel  15455  brstruct  17118  sscrel  17780  gaorber  19283  sylow2a  19594  efgrelexlemb  19725  efgcpbllemb  19730  rellindf  21788  psrbaglesupp  21902  2ndcctbss  23420  refrel  23473  vitalilem1  25575  lgsquadlem1  27343  lgsquadlem2  27344  dmcuts  27783  relsubgr  29338  vcrel  30631  h2hlm  31051  hlimi  31259  erler  33326  relfldext  33788  finextfldext  33808  relmntop  34168  relae  34384  fineqvnttrclse  35268  fnerel  36520  filnetlem3  36562  brabg2  38038  heiborlem3  38134  heiborlem4  38135  relrngo  38217  isdivrngo  38271  drngoi  38272  isdrngo1  38277  riscer  38309  relcoss  38834  relssr  38901  prter1  39325  prter3  39328  prjsper  43041  reldvds  44742  nelbrim  47723  rellininds  48919