| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ralbii2 | Structured version Visualization version GIF version | ||
| Description: Inference adding different restricted universal quantifiers to each side of an equivalence. (Contributed by NM, 15-Aug-2005.) |
| Ref | Expression |
|---|---|
| ralbii2.1 | ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐵 → 𝜓)) |
| Ref | Expression |
|---|---|
| ralbii2 | ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ralbii2.1 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐵 → 𝜓)) | |
| 2 | 1 | albii 1819 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) |
| 3 | df-ral 3062 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
| 4 | df-ral 3062 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) | |
| 5 | 2, 3, 4 | 3bitr4i 303 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 ∈ wcel 2108 ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-ral 3062 |
| This theorem is referenced by: ralbiia 3091 ralcom3 3097 raleqbii 3344 ralrab 3699 raldifb 4149 ralin 4249 raldifsni 4795 reusv2 5403 dfsup2 9484 iscard2 10016 acnnum 10092 dfac9 10177 dfacacn 10182 raluz2 12939 ralrp 13055 isprm4 16721 isdomn2OLD 20712 sdrgacs 20802 isnrm2 23366 ismbl 25561 ellimc3 25914 dchrelbas2 27281 h1dei 31569 iineq1i 36197 ixpeq1i 36201 fnwe2lem2 43063 |
| Copyright terms: Public domain | W3C validator |