Theorem opabssxp 5744

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

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

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 5168  df-xp 5658

This theorem is referenced by:  brab2a  5745  dmoprabss  7504  ecopovsym  8805  ecopovtrn  8806  ecopover  8807  enqex  10895  lterpq  10943  ltrelpr  10971  enrex  11040  ltrelsr  11041  ltrelre  11107  ltrelxr  11258  rlimpm  15541  dvdszrcl  16305  prdsle  17505  prdsless  17506  sectfval  17798  sectss  17799  ltbval  22154  opsrle  22158  lmfval  23350  isphtpc  25114  bcthlem1  25444  bcthlem5  25448  lgsquadlem1  27502  lgsquadlem2  27503  lgsquadlem3  27504  ishlg  28829  perpln1  28941  perpln2  28942  isperp  28943  iscgra  29061  isinag  29090  isleag  29099  inftmrel  33413  isinftm  33414  fldextfld1  33954  fldextfld2  33955  metidval  34197  metidss  34198  faeval  34553  filnetlem2  36752  numiunnum  36843  areacirc  38224  lcvfbr  39656  cmtfvalN  39846  cvrfval  39904  dicssdvh  41822  aks6d1c1p1rcl  42737  pellexlem3  43420  pellexlem4  43421  pellexlem5  43422  pellex  43424  rfovcnvf1od  44592  fsovrfovd  44597  sectfn  49658