Theorem opabssxp 5752

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

Syntax hints:   ∧ wa 395   ∈ wcel 2109   ⊆ wss 3931  {copab 5186   × cxp 5657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-ss 3948  df-opab 5187  df-xp 5665

This theorem is referenced by:  brab2a  5753  dmoprabss  7516  ecopovsym  8838  ecopovtrn  8839  ecopover  8840  enqex  10941  lterpq  10989  ltrelpr  11017  enrex  11086  ltrelsr  11087  ltrelre  11153  ltrelxr  11301  rlimpm  15521  dvdszrcl  16282  prdsle  17481  prdsless  17482  sectfval  17769  sectss  17770  ltbval  22006  opsrle  22010  lmfval  23175  isphtpc  24949  bcthlem1  25281  bcthlem5  25285  lgsquadlem1  27348  lgsquadlem2  27349  lgsquadlem3  27350  ishlg  28586  perpln1  28694  perpln2  28695  isperp  28696  iscgra  28793  isinag  28822  isleag  28831  inftmrel  33183  isinftm  33184  fldextfld1  33694  fldextfld2  33695  metidval  33926  metidss  33927  faeval  34282  filnetlem2  36402  numiunnum  36493  areacirc  37742  lcvfbr  39043  cmtfvalN  39233  cvrfval  39291  dicssdvh  41210  aks6d1c1p1rcl  42126  pellexlem3  42829  pellexlem4  42830  pellexlem5  42831  pellex  42833  rfovcnvf1od  44003  fsovrfovd  44008  sectfn  48979