Theorem opabssxp 5441

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 476	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2	1	ssopab2i 5240	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3		df-xp 5361	. 2 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
4	2, 3	sseqtr4i 3856	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)

Syntax hints:   ∧ wa 386   ∈ wcel 2106   ⊆ wss 3791  {copab 4948   × cxp 5353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-ext 2753

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-in 3798  df-ss 3805  df-opab 4949  df-xp 5361

This theorem is referenced by:  brab2a  5442  dmoprabss  7019  ecopovsym  8133  ecopovtrn  8134  ecopover  8135  enqex  10079  lterpq  10127  ltrelpr  10155  enrex  10224  ltrelsr  10225  ltrelre  10291  ltrelxr  10438  rlimpm  14639  dvdszrcl  15392  prdsle  16508  prdsless  16509  sectfval  16796  sectss  16797  ltbval  19868  opsrle  19872  lmfval  21444  isphtpc  23201  bcthlem1  23530  bcthlem5  23534  lgsquadlem1  25557  lgsquadlem2  25558  lgsquadlem3  25559  ishlg  25953  perpln1  26061  perpln2  26062  isperp  26063  iscgra  26157  isinag  26187  isleag  26196  inftmrel  30310  isinftm  30311  metidval  30545  metidss  30546  faeval  30921  filnetlem2  32976  areacirc  34124  lcvfbr  35168  cmtfvalN  35358  cvrfval  35416  dicssdvh  37334  pellexlem3  38347  pellexlem4  38348  pellexlem5  38349  pellex  38351  rfovcnvf1od  39246  fsovrfovd  39251