Theorem opabssxp 5781

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

Syntax hints:   ∧ wa 395   ∈ wcel 2106   ⊆ wss 3963  {copab 5210   × cxp 5687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-ss 3980  df-opab 5211  df-xp 5695

This theorem is referenced by:  brab2a  5782  dmoprabss  7536  ecopovsym  8858  ecopovtrn  8859  ecopover  8860  enqex  10960  lterpq  11008  ltrelpr  11036  enrex  11105  ltrelsr  11106  ltrelre  11172  ltrelxr  11320  rlimpm  15533  dvdszrcl  16292  prdsle  17509  prdsless  17510  sectfval  17799  sectss  17800  ltbval  22079  opsrle  22083  lmfval  23256  isphtpc  25040  bcthlem1  25372  bcthlem5  25376  lgsquadlem1  27439  lgsquadlem2  27440  lgsquadlem3  27441  ishlg  28625  perpln1  28733  perpln2  28734  isperp  28735  iscgra  28832  isinag  28861  isleag  28870  inftmrel  33170  isinftm  33171  fldextfld1  33677  fldextfld2  33678  metidval  33851  metidss  33852  faeval  34227  filnetlem2  36362  numiunnum  36453  areacirc  37700  lcvfbr  39002  cmtfvalN  39192  cvrfval  39250  dicssdvh  41169  aks6d1c1p1rcl  42090  pellexlem3  42819  pellexlem4  42820  pellexlem5  42821  pellex  42823  rfovcnvf1od  43994  fsovrfovd  43999