ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ceqsalt Structured version   GIF version

Theorem ceqsalt 2574
Description: Closed theorem version of ceqsalg 2576. (Contributed by NM, 28-Feb-2013.) (Revised by Mario Carneiro, 10-Oct-2016.)
Assertion
Ref Expression
ceqsalt ((Ⅎxψ x(x = A → (φψ)) A 𝑉) → (x(x = Aφ) ↔ ψ))
Distinct variable group:   x,A
Allowed substitution hints:   φ(x)   ψ(x)   𝑉(x)

Proof of Theorem ceqsalt
StepHypRef Expression
1 elisset 2562 . . . 4 (A 𝑉x x = A)
213ad2ant3 926 . . 3 ((Ⅎxψ x(x = A → (φψ)) A 𝑉) → x x = A)
3 bi1 111 . . . . . . 7 ((φψ) → (φψ))
43imim3i 55 . . . . . 6 ((x = A → (φψ)) → ((x = Aφ) → (x = Aψ)))
54al2imi 1344 . . . . 5 (x(x = A → (φψ)) → (x(x = Aφ) → x(x = Aψ)))
653ad2ant2 925 . . . 4 ((Ⅎxψ x(x = A → (φψ)) A 𝑉) → (x(x = Aφ) → x(x = Aψ)))
7 19.23t 1564 . . . . 5 (Ⅎxψ → (x(x = Aψ) ↔ (x x = Aψ)))
873ad2ant1 924 . . . 4 ((Ⅎxψ x(x = A → (φψ)) A 𝑉) → (x(x = Aψ) ↔ (x x = Aψ)))
96, 8sylibd 138 . . 3 ((Ⅎxψ x(x = A → (φψ)) A 𝑉) → (x(x = Aφ) → (x x = Aψ)))
102, 9mpid 37 . 2 ((Ⅎxψ x(x = A → (φψ)) A 𝑉) → (x(x = Aφ) → ψ))
11 bi2 121 . . . . . . 7 ((φψ) → (ψφ))
1211imim2i 12 . . . . . 6 ((x = A → (φψ)) → (x = A → (ψφ)))
1312com23 72 . . . . 5 ((x = A → (φψ)) → (ψ → (x = Aφ)))
1413alimi 1341 . . . 4 (x(x = A → (φψ)) → x(ψ → (x = Aφ)))
15143ad2ant2 925 . . 3 ((Ⅎxψ x(x = A → (φψ)) A 𝑉) → x(ψ → (x = Aφ)))
16 19.21t 1471 . . . 4 (Ⅎxψ → (x(ψ → (x = Aφ)) ↔ (ψx(x = Aφ))))
17163ad2ant1 924 . . 3 ((Ⅎxψ x(x = A → (φψ)) A 𝑉) → (x(ψ → (x = Aφ)) ↔ (ψx(x = Aφ))))
1815, 17mpbid 135 . 2 ((Ⅎxψ x(x = A → (φψ)) A 𝑉) → (ψx(x = Aφ)))
1910, 18impbid 120 1 ((Ⅎxψ x(x = A → (φψ)) A 𝑉) → (x(x = Aφ) ↔ ψ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98   w3a 884  wal 1240   = wceq 1242  wnf 1346  wex 1378   wcel 1390
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-3an 886  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-v 2553
This theorem is referenced by:  ceqsralt  2575
  Copyright terms: Public domain W3C validator