Theorem opabssxp 5773

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 481	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2	1	ssopab2i 5555	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3		df-xp 5687	. 2 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
4	2, 3	sseqtrri 4016	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)

Syntax hints:   ∧ wa 394   ∈ wcel 2098   ⊆ wss 3946  {copab 5214   × cxp 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-ss 3963  df-opab 5215  df-xp 5687

This theorem is referenced by:  brab2a  5774  dmoprabss  7527  ecopovsym  8847  ecopovtrn  8848  ecopover  8849  enqex  10961  lterpq  11009  ltrelpr  11037  enrex  11106  ltrelsr  11107  ltrelre  11173  ltrelxr  11321  rlimpm  15497  dvdszrcl  16256  prdsle  17472  prdsless  17473  sectfval  17762  sectss  17763  ltbval  22042  opsrle  22046  lmfval  23219  isphtpc  25003  bcthlem1  25335  bcthlem5  25339  lgsquadlem1  27401  lgsquadlem2  27402  lgsquadlem3  27403  ishlg  28521  perpln1  28629  perpln2  28630  isperp  28631  iscgra  28728  isinag  28757  isleag  28766  inftmrel  33022  isinftm  33023  fldextfld1  33510  fldextfld2  33511  metidval  33661  metidss  33662  faeval  34035  filnetlem2  36039  areacirc  37362  lcvfbr  38666  cmtfvalN  38856  cvrfval  38914  dicssdvh  40833  aks6d1c1p1rcl  41754  pellexlem3  42425  pellexlem4  42426  pellexlem5  42427  pellex  42429  rfovcnvf1od  43608  fsovrfovd  43613