![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvalv1 | Structured version Visualization version GIF version |
Description: Version of cbval 2423 with a disjoint variable condition, which does not require ax-13 2389. See cbvalvw 2143 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvalv 2425 for another variant. (Contributed by BJ, 31-May-2019.) |
Ref | Expression |
---|---|
cbvalv1.nf1 | ⊢ Ⅎ𝑦𝜑 |
cbvalv1.nf2 | ⊢ Ⅎ𝑥𝜓 |
cbvalv1.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvalv1 | ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvalv1.nf1 | . . 3 ⊢ Ⅎ𝑦𝜑 | |
2 | cbvalv1.nf2 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
3 | cbvalv1.1 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
4 | 3 | biimpd 221 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) |
5 | 1, 2, 4 | cbv3v 2365 | . 2 ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) |
6 | 3 | biimprd 240 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜓 → 𝜑)) |
7 | 6 | equcoms 2124 | . . 3 ⊢ (𝑦 = 𝑥 → (𝜓 → 𝜑)) |
8 | 2, 1, 7 | cbv3v 2365 | . 2 ⊢ (∀𝑦𝜓 → ∀𝑥𝜑) |
9 | 5, 8 | impbii 201 | 1 ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∀wal 1654 Ⅎwnf 1882 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-10 2192 ax-11 2207 ax-12 2220 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1879 df-nf 1883 |
This theorem is referenced by: cbvexv1 2368 sb8v 2376 sb8eulem 2686 cleqh 2929 cbvralf 3377 ralab2 3594 cbvralcsf 3789 dfss2f 3818 elintab 4710 reusv2lem4 5103 cbviota 6095 sb8iota 6097 dffun6f 6141 findcard2 8475 aceq1 9260 bnj1385 31445 bj-cbvalvv 33265 bj-cbval2v 33269 bj-abbi 33299 sbcalf 34457 alrimii 34463 aomclem6 38471 rababg 38719 |
Copyright terms: Public domain | W3C validator |