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 2398 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 1911 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) | |
2 | ax-5 1911 | . 2 ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) | |
3 | ax-5 1911 | . 2 ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓) | |
4 | ax-5 1911 | . 2 ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑) | |
5 | cbvalvw.1 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
6 | 1, 2, 3, 4, 5 | cbvalw 2036 | 1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∀wal 1537 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1780 |
This theorem is referenced by: cbvexvw 2038 cbvaldvaw 2039 cbval2vw 2041 alcomiw 2044 hba1w 2048 sbjust 2064 ax12wdemo 2129 mo4 2564 cbvmovw 2600 nfcjust 2886 cbvralvw 3222 cbvraldva2 3404 zfpow 5298 tfisi 7737 findcard 8984 pssnn 8989 ssfi 8994 pssnnOLD 9086 findcard3 9105 zfinf 9445 ttrclss 9526 ttrclselem2 9532 aceq0 9924 kmlem1 9956 kmlem13 9968 fin23lem32 10150 fin23lem41 10158 zfac 10266 zfcndpow 10422 zfcndinf 10424 zfcndac 10425 axgroth4 10638 relexpindlem 14823 ramcl 16779 mreexexlemd 17402 bnj1112 33012 dfon2lem6 33813 dfon2lem7 33814 dfon2 33817 phpreu 35809 axc11n-16 37152 dfac11 41083 ismnushort 42132 |
Copyright terms: Public domain | W3C validator |