Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  reeanlem Structured version   Visualization version   GIF version

Theorem reeanlem 3284
 Description: Lemma factoring out common proof steps of reeanv 3286 and reean 3285. (Contributed by Wolf Lammen, 20-Aug-2023.)
Hypothesis
Ref Expression
reeanlem.1 (∃𝑥𝑦((𝑥𝐴𝜑) ∧ (𝑦𝐵𝜓)) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃𝑦(𝑦𝐵𝜓)))
Assertion
Ref Expression
reeanlem (∃𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑 ∧ ∃𝑦𝐵 𝜓))
Distinct variable groups:   𝑦,𝐴   𝑥,𝐵   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑦)

Proof of Theorem reeanlem
StepHypRef Expression
1 an4 656 . . . 4 (((𝑥𝐴𝑦𝐵) ∧ (𝜑𝜓)) ↔ ((𝑥𝐴𝜑) ∧ (𝑦𝐵𝜓)))
212exbii 1851 . . 3 (∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ (𝜑𝜓)) ↔ ∃𝑥𝑦((𝑥𝐴𝜑) ∧ (𝑦𝐵𝜓)))
3 reeanlem.1 . . 3 (∃𝑥𝑦((𝑥𝐴𝜑) ∧ (𝑦𝐵𝜓)) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃𝑦(𝑦𝐵𝜓)))
42, 3bitri 278 . 2 (∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ (𝜑𝜓)) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃𝑦(𝑦𝐵𝜓)))
5 r2ex 3228 . 2 (∃𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ ∃𝑥𝑦((𝑥𝐴𝑦𝐵) ∧ (𝜑𝜓)))
6 df-rex 3077 . . 3 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
7 df-rex 3077 . . 3 (∃𝑦𝐵 𝜓 ↔ ∃𝑦(𝑦𝐵𝜓))
86, 7anbi12i 630 . 2 ((∃𝑥𝐴 𝜑 ∧ ∃𝑦𝐵 𝜓) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃𝑦(𝑦𝐵𝜓)))
94, 5, 83bitr4i 307 1 (∃𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑 ∧ ∃𝑦𝐵 𝜓))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 400  ∃wex 1782   ∈ wcel 2112  ∃wrex 3072 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912 This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-ral 3076  df-rex 3077 This theorem is referenced by:  reean  3285  reeanv  3286
 Copyright terms: Public domain W3C validator