![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvalvw | Structured version Visualization version GIF version |
Description: Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2395 for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Feb-2018.) |
Ref | Expression |
---|---|
cbvalvw.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvalvw | ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1906 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) | |
2 | ax-5 1906 | . 2 ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) | |
3 | ax-5 1906 | . 2 ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓) | |
4 | ax-5 1906 | . 2 ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑) | |
5 | cbvalvw.1 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 1, 2, 3, 4, 5 | cbvalw 2031 | 1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∀wal 1532 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1775 |
This theorem is referenced by: cbvexvw 2033 cbvaldvaw 2034 cbval2vw 2036 alcomiw 2039 hba1w 2043 sbjust 2059 ax12wdemo 2124 mo4 2556 cbvmovw 2592 nfcjust 2880 cbvralvw 3230 cbvraldva2 3340 sbralie 3350 zfpow 5360 tfisi 7857 findcard 9181 pssnn 9186 ssfi 9191 pssnnOLD 9283 findcard3 9303 findcard3OLD 9304 zfinf 9656 ttrclss 9737 ttrclselem2 9743 aceq0 10135 kmlem1 10167 kmlem13 10179 fin23lem32 10361 fin23lem41 10369 zfac 10477 zfcndpow 10633 zfcndinf 10635 zfcndac 10636 axgroth4 10849 relexpindlem 15036 ramcl 16991 mreexexlemd 17617 bnj1112 34608 dfon2lem6 35378 dfon2lem7 35379 dfon2 35382 phpreu 37071 axc11n-16 38404 dfac11 42480 ismnushort 43732 |
Copyright terms: Public domain | W3C validator |