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 1811 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) |
3 | df-ral 3140 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
4 | df-ral 3140 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) | |
5 | 2, 3, 4 | 3bitr4i 304 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∀wal 1526 ∈ wcel 2105 ∀wral 3135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 |
This theorem depends on definitions: df-bi 208 df-ral 3140 |
This theorem is referenced by: ralbiia 3161 ralbii 3162 raleqbii 3231 ralrab 3682 raldifb 4118 raldifsni 4720 reusv2 5294 dfsup2 8896 iscard2 9393 acnnum 9466 dfac9 9550 dfacacn 9555 raluz2 12285 ralrp 12397 isprm4 16016 sdrgacs 19509 isdomn2 20000 isnrm2 21894 ismbl 24054 ellimc3 24404 dchrelbas2 25740 h1dei 29254 fnwe2lem2 39529 |
Copyright terms: Public domain | W3C validator |