Theorem opabssxp 5755

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 487	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2	1	ssopab2i 5537	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3		df-xp 5669	. 2 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
4	2, 3	sseqtrri 3987	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)

Syntax hints:   ∧ wa 400   ∈ wcel 2143   ⊆ wss 3906  {copab 5174   × cxp 5661

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-ss 3923  df-opab 5175  df-xp 5669

This theorem is referenced by:  brab2a  5756  dmoprabss  7516  ecopovsym  8818  ecopovtrn  8819  ecopover  8820  enqex  10908  lterpq  10956  ltrelpr  10984  enrex  11053  ltrelsr  11054  ltrelre  11120  ltrelxr  11271  rlimpm  15553  dvdszrcl  16316  prdsle  17516  prdsless  17517  sectfval  17809  sectss  17810  ltbval  22175  opsrle  22179  lmfval  23370  isphtpc  25134  bcthlem1  25464  bcthlem5  25468  lgsquadlem1  27525  lgsquadlem2  27526  lgsquadlem3  27527  ishlg2  28852  ishlg  28855  perpln1  28971  perpln2  28972  isperp  28973  iscgra  29101  isinag  29136  isleag  29145  inftmrel  33481  isinftm  33482  fldextfld1  34018  fldextfld2  34019  metidval  34261  metidss  34262  faeval  34617  filnetlem2  36871  numiunnum  36962  areacirc  38345  lcvfbr  39775  cmtfvalN  39965  cvrfval  40023  dicssdvh  41941  aks6d1c1p1rcl  42856  pellexlem3  43541  pellexlem4  43542  pellexlem5  43543  pellex  43545  rfovcnvf1od  44713  fsovrfovd  44718  sectfn  49790