Theorem opabssxp 5743

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

Syntax hints:   ∧ wa 400   ∈ wcel 2145   ⊆ wss 3907  {copab 5166   × cxp 5649

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-ss 3924  df-opab 5167  df-xp 5657

This theorem is referenced by:  brab2a  5744  dmoprabss  7504  ecopovsym  8805  ecopovtrn  8806  ecopover  8807  enqex  10895  lterpq  10943  ltrelpr  10971  enrex  11040  ltrelsr  11041  ltrelre  11107  ltrelxr  11258  rlimpm  15539  dvdszrcl  16303  prdsle  17503  prdsless  17504  sectfval  17796  sectss  17797  ltbval  22151  opsrle  22155  lmfval  23346  isphtpc  25110  bcthlem1  25440  bcthlem5  25444  lgsquadlem1  27498  lgsquadlem2  27499  lgsquadlem3  27500  ishlg  28825  perpln1  28937  perpln2  28938  isperp  28939  iscgra  29057  isinag  29086  isleag  29095  inftmrel  33408  isinftm  33409  fldextfld1  33949  fldextfld2  33950  metidval  34192  metidss  34193  faeval  34548  filnetlem2  36747  numiunnum  36838  areacirc  38219  lcvfbr  39651  cmtfvalN  39841  cvrfval  39899  dicssdvh  41817  aks6d1c1p1rcl  42732  pellexlem3  43415  pellexlem4  43416  pellexlem5  43417  pellex  43419  rfovcnvf1od  44587  fsovrfovd  44592  sectfn  49659