|   | 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 2405 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 1910 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) | |
| 2 | ax-5 1910 | . 2 ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) | |
| 3 | ax-5 1910 | . 2 ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓) | |
| 4 | ax-5 1910 | . 2 ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑) | |
| 5 | cbvalvw.1 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
| 6 | 1, 2, 3, 4, 5 | cbvalw 2034 | 1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∀wal 1538 | 
| 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 1910 ax-6 1967 ax-7 2007 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 | 
| This theorem is referenced by: cbvexvw 2036 cbvaldvaw 2037 cbval2vw 2039 alcomimw 2042 hba1w 2047 sbjust 2063 ax12wdemo 2135 mo4 2566 cbvmovw 2602 nfcjust 2891 cbvralvw 3237 cbvraldva2 3348 sbralie 3358 zfpow 5366 tfisi 7880 findcard 9203 pssnn 9208 ssfi 9213 findcard3 9318 findcard3OLD 9319 zfinf 9679 ttrclss 9760 ttrclselem2 9766 aceq0 10158 kmlem1 10191 kmlem13 10203 fin23lem32 10384 fin23lem41 10392 zfac 10500 zfcndpow 10656 zfcndinf 10658 zfcndac 10659 axgroth4 10872 relexpindlem 15102 ramcl 17067 mreexexlemd 17687 bnj1112 34997 dfon2lem6 35789 dfon2lem7 35790 dfon2 35793 cbvralvw2 36227 phpreu 37611 axc11n-16 38939 nfa1w 42685 eu6w 42686 abbibw 42687 dfac11 43074 ismnushort 44320 modelaxrep 44998 | 
| Copyright terms: Public domain | W3C validator |