Theorem opabssxp 5679

Description: An abstraction relation is a subset of a related Cartesian product. (Contributed by NM, 16-Jul-1995.)

Assertion

Ref	Expression
opabssxp	⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem opabssxp

Step	Hyp	Ref	Expression
1		simpl 483	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2	1	ssopab2i 5463	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3		df-xp 5595	. 2 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
4	2, 3	sseqtrri 3958	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)

Syntax hints:   ∧ wa 396   ∈ wcel 2106   ⊆ wss 3887  {copab 5136   × cxp 5587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-opab 5137  df-xp 5595

This theorem is referenced by:  brab2a  5680  dmoprabss  7377  ecopovsym  8608  ecopovtrn  8609  ecopover  8610  enqex  10678  lterpq  10726  ltrelpr  10754  enrex  10823  ltrelsr  10824  ltrelre  10890  ltrelxr  11036  rlimpm  15209  dvdszrcl  15968  prdsle  17173  prdsless  17174  sectfval  17463  sectss  17464  ltbval  21244  opsrle  21248  lmfval  22383  isphtpc  24157  bcthlem1  24488  bcthlem5  24492  lgsquadlem1  26528  lgsquadlem2  26529  lgsquadlem3  26530  ishlg  26963  perpln1  27071  perpln2  27072  isperp  27073  iscgra  27170  isinag  27199  isleag  27208  inftmrel  31434  isinftm  31435  fldextfld1  31724  fldextfld2  31725  metidval  31840  metidss  31841  faeval  32214  filnetlem2  34568  areacirc  35870  lcvfbr  37034  cmtfvalN  37224  cvrfval  37282  dicssdvh  39200  pellexlem3  40653  pellexlem4  40654  pellexlem5  40655  pellex  40657  rfovcnvf1od  41612  fsovrfovd  41617