| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cbvralvw | GIF version | ||
| Description: Version of cbvralv 2767 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.) |
| Ref | Expression |
|---|---|
| cbvralvw.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| cbvralvw | ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq1w 2292 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
| 2 | cbvralvw.1 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
| 3 | 1, 2 | imbi12d 234 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓))) |
| 4 | 3 | cbvalvw 1968 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) |
| 5 | df-ral 2515 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
| 6 | df-ral 2515 | . 2 ⊢ (∀𝑦 ∈ 𝐴 𝜓 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜓)) | |
| 7 | 4, 5, 6 | 3bitr4i 212 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ 𝐴 𝜓) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ↔ wb 105 ∀wal 1395 ∈ wcel 2202 ∀wral 2510 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1495 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 |
| This theorem depends on definitions: df-bi 117 df-nf 1509 df-clel 2227 df-ral 2515 |
| This theorem is referenced by: cbvral2vw 2778 cc1 7484 zsupssdc 10499 wrdind 11307 wrd2ind 11308 reuccatpfxs1 11332 prmpwdvds 12946 nninfdclemcl 13087 grpinvalem 13486 grpinva 13487 issubg4m 13798 isnsg2 13808 elnmz 13813 fsumdvdsmul 15734 2sqlem6 15868 2sqlem10 15873 uspgr2wlkeq 16235 depindlem1 16376 bj-charfunbi 16457 |
| Copyright terms: Public domain | W3C validator |