Theorem sbal 1345

Description: Move universal quantifier in and out of substitution.

Assertion

Ref	Expression
sbal	⊢ ([z / y]∀xφ ↔ ∀x[z / y]φ)

Distinct variable groups:   x,y   x,z

Proof of Theorem sbal

Step	Hyp	Ref	Expression
1		a16gb 1275	. . . . 5 ⊢ (∀x x = z → (φ ↔ ∀xφ))
2	1	sbimi 1171	. . . 4 ⊢ ([z / y]∀x x = z → [z / y](φ ↔ ∀xφ))
3		sbequ5 1188	. . . 4 ⊢ ([z / y]∀x x = z ↔ ∀x x = z)
4		sbbi 1237	. . . 4 ⊢ ([z / y](φ ↔ ∀xφ) ↔ ([z / y]φ ↔ [z / y]∀xφ))
5	2, 3, 4	3imtr3 218	. . 3 ⊢ (∀x x = z → ([z / y]φ ↔ [z / y]∀xφ))
6		a16gb 1275	. . 3 ⊢ (∀x x = z → ([z / y]φ ↔ ∀x[z / y]φ))
7	5, 6	bitr3d 529	. 2 ⊢ (∀x x = z → ([z / y]∀xφ ↔ ∀x[z / y]φ))
8		sbal1 1344	. 2 ⊢ (¬ ∀x x = z → ([z / y]∀xφ ↔ ∀x[z / y]φ))
9	7, 8	pm2.61i 126	1 ⊢ ([z / y]∀xφ ↔ ∀x[z / y]φ)

Syntax hints:   ↔ wb 146  ∀wal 952  [wsbc 1168

This theorem is referenced by:  sbex 1346  sbalv 1347  sbabel 1581  sbcalg 1970

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-12 966  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170

Copyright terms: Public domain