Theorem opabssxp 5723

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

Syntax hints:   ∧ wa 395   ∈ wcel 2114   ⊆ wss 3889  {copab 5147   × cxp 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-ss 3906  df-opab 5148  df-xp 5637

This theorem is referenced by:  brab2a  5724  dmoprabss  7471  ecopovsym  8766  ecopovtrn  8767  ecopover  8768  enqex  10845  lterpq  10893  ltrelpr  10921  enrex  10990  ltrelsr  10991  ltrelre  11057  ltrelxr  11206  rlimpm  15462  dvdszrcl  16226  prdsle  17425  prdsless  17426  sectfval  17718  sectss  17719  ltbval  22021  opsrle  22025  lmfval  23197  isphtpc  24961  bcthlem1  25291  bcthlem5  25295  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  ishlg  28670  perpln1  28778  perpln2  28779  isperp  28780  iscgra  28877  isinag  28906  isleag  28915  inftmrel  33241  isinftm  33242  fldextfld1  33791  fldextfld2  33792  metidval  34034  metidss  34035  faeval  34390  filnetlem2  36561  numiunnum  36652  areacirc  38034  lcvfbr  39466  cmtfvalN  39656  cvrfval  39714  dicssdvh  41632  aks6d1c1p1rcl  42547  pellexlem3  43259  pellexlem4  43260  pellexlem5  43261  pellex  43263  rfovcnvf1od  44431  fsovrfovd  44436  sectfn  49504