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 2409 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 1902 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) | |
2 | ax-5 1902 | . 2 ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) | |
3 | ax-5 1902 | . 2 ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓) | |
4 | ax-5 1902 | . 2 ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑) | |
5 | cbvalvw.1 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 1, 2, 3, 4, 5 | cbvalw 2033 | 1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∀wal 1526 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 |
This theorem is referenced by: cbvexvw 2035 cbvaldvaw 2036 cbval2vw 2038 alcomiw 2041 hba1w 2045 sbjust 2059 ax12wdemo 2130 mo4 2643 nfcjust 2959 cbvralvw 3447 cbvraldva2 3454 cbvrexdva2OLD 3456 zfpow 5258 tfisi 7562 pssnn 8724 findcard 8745 findcard3 8749 zfinf 9090 aceq0 9532 kmlem1 9564 kmlem13 9576 fin23lem32 9754 fin23lem41 9762 zfac 9870 zfcndpow 10026 zfcndinf 10028 zfcndac 10029 axgroth4 10242 relexpindlem 14410 ramcl 16353 mreexexlemd 16903 bnj1112 32152 dfon2lem6 32930 dfon2lem7 32931 dfon2 32934 phpreu 34757 axc11n-16 35954 dfac11 39540 |
Copyright terms: Public domain | W3C validator |