Theorem opabssxp 5778

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

Syntax hints:   ∧ wa 395   ∈ wcel 2108   ⊆ wss 3951  {copab 5205   × cxp 5683

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-ss 3968  df-opab 5206  df-xp 5691

This theorem is referenced by:  brab2a  5779  dmoprabss  7537  ecopovsym  8859  ecopovtrn  8860  ecopover  8861  enqex  10962  lterpq  11010  ltrelpr  11038  enrex  11107  ltrelsr  11108  ltrelre  11174  ltrelxr  11322  rlimpm  15536  dvdszrcl  16295  prdsle  17507  prdsless  17508  sectfval  17795  sectss  17796  ltbval  22061  opsrle  22065  lmfval  23240  isphtpc  25026  bcthlem1  25358  bcthlem5  25362  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  ishlg  28610  perpln1  28718  perpln2  28719  isperp  28720  iscgra  28817  isinag  28846  isleag  28855  inftmrel  33187  isinftm  33188  fldextfld1  33700  fldextfld2  33701  metidval  33889  metidss  33890  faeval  34247  filnetlem2  36380  numiunnum  36471  areacirc  37720  lcvfbr  39021  cmtfvalN  39211  cvrfval  39269  dicssdvh  41188  aks6d1c1p1rcl  42109  pellexlem3  42842  pellexlem4  42843  pellexlem5  42844  pellex  42846  rfovcnvf1od  44017  fsovrfovd  44022