Theorem opabssxp 5724

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

Syntax hints:   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3903  {copab 5162   × cxp 5630

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-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-ss 3920  df-opab 5163  df-xp 5638

This theorem is referenced by:  brab2a  5725  dmoprabss  7472  ecopovsym  8768  ecopovtrn  8769  ecopover  8770  enqex  10845  lterpq  10893  ltrelpr  10921  enrex  10990  ltrelsr  10991  ltrelre  11057  ltrelxr  11205  rlimpm  15435  dvdszrcl  16196  prdsle  17394  prdsless  17395  sectfval  17687  sectss  17688  ltbval  22010  opsrle  22014  lmfval  23188  isphtpc  24961  bcthlem1  25292  bcthlem5  25296  lgsquadlem1  27359  lgsquadlem2  27360  lgsquadlem3  27361  ishlg  28686  perpln1  28794  perpln2  28795  isperp  28796  iscgra  28893  isinag  28922  isleag  28931  inftmrel  33273  isinftm  33274  fldextfld1  33824  fldextfld2  33825  metidval  34067  metidss  34068  faeval  34423  filnetlem2  36592  numiunnum  36683  areacirc  37958  lcvfbr  39390  cmtfvalN  39580  cvrfval  39638  dicssdvh  41556  aks6d1c1p1rcl  42472  pellexlem3  43182  pellexlem4  43183  pellexlem5  43184  pellex  43186  rfovcnvf1od  44354  fsovrfovd  44359  sectfn  49382