Theorem opabssxp 5708

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

Syntax hints:   ∧ wa 395   ∈ wcel 2111   ⊆ wss 3902  {copab 5153   × cxp 5614

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 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-ss 3919  df-opab 5154  df-xp 5622

This theorem is referenced by:  brab2a  5709  dmoprabss  7450  ecopovsym  8743  ecopovtrn  8744  ecopover  8745  enqex  10810  lterpq  10858  ltrelpr  10886  enrex  10955  ltrelsr  10956  ltrelre  11022  ltrelxr  11170  rlimpm  15404  dvdszrcl  16165  prdsle  17363  prdsless  17364  sectfval  17655  sectss  17656  ltbval  21976  opsrle  21980  lmfval  23145  isphtpc  24918  bcthlem1  25249  bcthlem5  25253  lgsquadlem1  27316  lgsquadlem2  27317  lgsquadlem3  27318  ishlg  28578  perpln1  28686  perpln2  28687  isperp  28688  iscgra  28785  isinag  28814  isleag  28823  inftmrel  33144  isinftm  33145  fldextfld1  33655  fldextfld2  33656  metidval  33898  metidss  33899  faeval  34254  filnetlem2  36412  numiunnum  36503  areacirc  37752  lcvfbr  39058  cmtfvalN  39248  cvrfval  39306  dicssdvh  41224  aks6d1c1p1rcl  42140  pellexlem3  42863  pellexlem4  42864  pellexlem5  42865  pellex  42867  rfovcnvf1od  44036  fsovrfovd  44041  sectfn  49060