New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  cbvex GIF version

Theorem cbvex 1985
 Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
cbvex.1 yφ
cbvex.2 xψ
cbvex.3 (x = y → (φψ))
Assertion
Ref Expression
cbvex (xφyψ)

Proof of Theorem cbvex
StepHypRef Expression
1 cbvex.1 . . . . 5 yφ
21nfn 1793 . . . 4 y ¬ φ
3 cbvex.2 . . . . 5 xψ
43nfn 1793 . . . 4 x ¬ ψ
5 cbvex.3 . . . . 5 (x = y → (φψ))
65notbid 285 . . . 4 (x = y → (¬ φ ↔ ¬ ψ))
72, 4, 6cbval 1984 . . 3 (x ¬ φy ¬ ψ)
87notbii 287 . 2 x ¬ φ ↔ ¬ y ¬ ψ)
9 df-ex 1542 . 2 (xφ ↔ ¬ x ¬ φ)
10 df-ex 1542 . 2 (yψ ↔ ¬ y ¬ ψ)
118, 9, 103bitr4i 268 1 (xφyψ)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176  ∀wal 1540  ∃wex 1541  Ⅎwnf 1544 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925 This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545 This theorem is referenced by:  cbvexv  2003  cbvex2  2005  exsb  2130  euf  2210  mo  2226  cbvmo  2241  mopick  2266  clelab  2473  issetf  2864  eqvincf  2967  rexab2  3003  euabsn  3792  eluniab  3903  cbvopab1  4632  cbvopab2  4633  cbvopab1s  4634  opeliunxp  4820  dfdmf  4905  dfrnf  4962  cbvoprab1  5567  cbvoprab2  5568
 Copyright terms: Public domain W3C validator