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

Theorem ceqsex2v 3529
Description: Elimination of two existential quantifiers, using implicit substitution. (Contributed by Scott Fenton, 7-Jun-2006.) Avoid ax-10 2146 and ax-11 2162. (Revised by Gino Giotto, 20-Aug-2023.)
Hypotheses
Ref Expression
ceqsex2v.1 𝐴 ∈ V
ceqsex2v.2 𝐵 ∈ V
ceqsex2v.3 (𝑥 = 𝐴 → (𝜑𝜓))
ceqsex2v.4 (𝑦 = 𝐵 → (𝜓𝜒))
Assertion
Ref Expression
ceqsex2v (∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵𝜑) ↔ 𝜒)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝜓,𝑥   𝜒,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)   𝜒(𝑥)

Proof of Theorem ceqsex2v
StepHypRef Expression
1 3anass 1092 . . . . 5 ((𝑥 = 𝐴𝑦 = 𝐵𝜑) ↔ (𝑥 = 𝐴 ∧ (𝑦 = 𝐵𝜑)))
21exbii 1849 . . . 4 (∃𝑦(𝑥 = 𝐴𝑦 = 𝐵𝜑) ↔ ∃𝑦(𝑥 = 𝐴 ∧ (𝑦 = 𝐵𝜑)))
3 19.42v 1955 . . . 4 (∃𝑦(𝑥 = 𝐴 ∧ (𝑦 = 𝐵𝜑)) ↔ (𝑥 = 𝐴 ∧ ∃𝑦(𝑦 = 𝐵𝜑)))
42, 3bitri 278 . . 3 (∃𝑦(𝑥 = 𝐴𝑦 = 𝐵𝜑) ↔ (𝑥 = 𝐴 ∧ ∃𝑦(𝑦 = 𝐵𝜑)))
54exbii 1849 . 2 (∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵𝜑) ↔ ∃𝑥(𝑥 = 𝐴 ∧ ∃𝑦(𝑦 = 𝐵𝜑)))
6 ceqsex2v.1 . . 3 𝐴 ∈ V
7 ceqsex2v.3 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜓))
87anbi2d 631 . . . 4 (𝑥 = 𝐴 → ((𝑦 = 𝐵𝜑) ↔ (𝑦 = 𝐵𝜓)))
98exbidv 1923 . . 3 (𝑥 = 𝐴 → (∃𝑦(𝑦 = 𝐵𝜑) ↔ ∃𝑦(𝑦 = 𝐵𝜓)))
106, 9ceqsexv 3526 . 2 (∃𝑥(𝑥 = 𝐴 ∧ ∃𝑦(𝑦 = 𝐵𝜑)) ↔ ∃𝑦(𝑦 = 𝐵𝜓))
11 ceqsex2v.2 . . 3 𝐵 ∈ V
12 ceqsex2v.4 . . 3 (𝑦 = 𝐵 → (𝜓𝜒))
1311, 12ceqsexv 3526 . 2 (∃𝑦(𝑦 = 𝐵𝜓) ↔ 𝜒)
145, 10, 133bitri 300 1 (∃𝑥𝑦(𝑥 = 𝐴𝑦 = 𝐵𝜑) ↔ 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wex 1781  wcel 2115  Vcvv 3479
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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-nf 1786  df-cleq 2817  df-clel 2896
This theorem is referenced by:  ceqsex3v  3530  ceqsex4v  3531  ispos  17546  elfuns  33394  brimg  33416  brapply  33417  brsuccf  33420  brrestrict  33428  dfrdg4  33430  diblsmopel  38367
  Copyright terms: Public domain W3C validator