Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-ceqsalt Structured version   Unicode version

Theorem bj-ceqsalt 34637
Description: Remove from ceqsalt 3132 dependency on ax-ext 2435 (and on df-cleq 2449 and df-v 3111). Note: this is not doable with ceqsralt 3133 (or ceqsralv 3138), which uses eleq1 2529, but the same dependence removal is possible for ceqsalg 3134, ceqsal 3136, ceqsalv 3137, cgsexg 3142, cgsex2g 3143, cgsex4g 3144, ceqsex 3145, ceqsexv 3146, ceqsex2 3147, ceqsex2v 3148, ceqsex3v 3149, ceqsex4v 3150, ceqsex6v 3151, ceqsex8v 3152, gencbvex 3153 (after changing  A  =  y to  y  =  A), gencbvex2 3154, gencbval 3155, vtoclgft 3157 (it uses  F/_, whose justification nfcjust 2606 is actually provable without ax-ext 2435, as bj-nfcjust 34612 shows) and several other vtocl* theorems (see for instance bj-vtoclg1f 34669). See also bj-ceqsaltv 34638. (Contributed by BJ, 16-Jun-2019.) (Proof modification is discouraged.)
Assertion
Ref Expression
bj-ceqsalt  |-  ( ( F/ x ps  /\  A. x ( x  =  A  ->  ( ph  <->  ps ) )  /\  A  e.  V )  ->  ( A. x ( x  =  A  ->  ph )  <->  ps )
)
Distinct variable group:    x, A
Allowed substitution hints:    ph( x)    ps( x)    V( x)

Proof of Theorem bj-ceqsalt
StepHypRef Expression
1 bj-elisset 34624 . . 3  |-  ( A  e.  V  ->  E. x  x  =  A )
213anim3i 1184 . 2  |-  ( ( F/ x ps  /\  A. x ( x  =  A  ->  ( ph  <->  ps ) )  /\  A  e.  V )  ->  ( F/ x ps  /\  A. x ( x  =  A  ->  ( ph  <->  ps ) )  /\  E. x  x  =  A
) )
3 bj-ceqsalt0 34635 . 2  |-  ( ( F/ x ps  /\  A. x ( x  =  A  ->  ( ph  <->  ps ) )  /\  E. x  x  =  A
)  ->  ( A. x ( x  =  A  ->  ph )  <->  ps )
)
42, 3syl 16 1  |-  ( ( F/ x ps  /\  A. x ( x  =  A  ->  ( ph  <->  ps ) )  /\  A  e.  V )  ->  ( A. x ( x  =  A  ->  ph )  <->  ps )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ w3a 973   A.wal 1393    = wceq 1395   E.wex 1613   F/wnf 1617    e. wcel 1819
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-12 1855
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-clel 2452
This theorem is referenced by:  bj-ceqsalgALT  34641
  Copyright terms: Public domain W3C validator