Theorem opabssxp 5116

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 472	. . 3 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
2	1	ssopab2i 4928	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
3		df-xp 5044	. 2 ⊢ (𝐴 × 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)}
4	2, 3	sseqtr4i 3601	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑)} ⊆ (𝐴 × 𝐵)

Syntax hints:   ∧ wa 383   ∈ wcel 1977   ⊆ wss 3540  {copab 4642   × cxp 5036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554  df-opab 4644  df-xp 5044

This theorem is referenced by:  brab2ga  5117  dmoprabss  6640  ecopovsym  7736  ecopovtrn  7737  ecopover  7738  ecopoverOLD  7739  enqex  9623  lterpq  9671  ltrelpr  9699  enrex  9767  ltrelsr  9768  ltrelre  9834  ltrelxr  9978  rlimpm  14079  dvdszrcl  14826  prdsle  15945  prdsless  15946  sectfval  16234  sectss  16235  ltbval  19292  opsrle  19296  lmfval  20846  isphtpc  22601  bcthlem1  22929  bcthlem5  22933  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  ishlg  25297  perpln1  25405  perpln2  25406  isperp  25407  iscgra  25501  isinag  25529  isleag  25533  inftmrel  29065  isinftm  29066  metidval  29261  metidss  29262  faeval  29636  filnetlem2  31544  areacirc  32675  lcvfbr  33325  cmtfvalN  33515  cvrfval  33573  dicssdvh  35493  pellexlem3  36413  pellexlem4  36414  pellexlem5  36415  pellex  36417  rfovcnvf1od  37318  fsovrfovd  37323