Theorem opabssxp 5711

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 5493	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3		df-xp 5625	. 2 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
4	2, 3	sseqtrri 3980	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)

Syntax hints:   ∧ wa 395   ∈ wcel 2113   ⊆ wss 3898  {copab 5155   × cxp 5617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-ss 3915  df-opab 5156  df-xp 5625

This theorem is referenced by:  brab2a  5712  dmoprabss  7456  ecopovsym  8749  ecopovtrn  8750  ecopover  8751  enqex  10820  lterpq  10868  ltrelpr  10896  enrex  10965  ltrelsr  10966  ltrelre  11032  ltrelxr  11180  rlimpm  15409  dvdszrcl  16170  prdsle  17368  prdsless  17369  sectfval  17660  sectss  17661  ltbval  21979  opsrle  21983  lmfval  23148  isphtpc  24921  bcthlem1  25252  bcthlem5  25256  lgsquadlem1  27319  lgsquadlem2  27320  lgsquadlem3  27321  ishlg  28581  perpln1  28689  perpln2  28690  isperp  28691  iscgra  28788  isinag  28817  isleag  28826  inftmrel  33156  isinftm  33157  fldextfld1  33681  fldextfld2  33682  metidval  33924  metidss  33925  faeval  34280  filnetlem2  36444  numiunnum  36535  areacirc  37773  lcvfbr  39139  cmtfvalN  39329  cvrfval  39387  dicssdvh  41305  aks6d1c1p1rcl  42221  pellexlem3  42948  pellexlem4  42949  pellexlem5  42950  pellex  42952  rfovcnvf1od  44121  fsovrfovd  44126  sectfn  49154