![]() |
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 1813 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) |
3 | df-ral 3051 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
4 | df-ral 3051 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) | |
5 | 2, 3, 4 | 3bitr4i 302 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1531 ∈ wcel 2098 ∀wral 3050 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 |
This theorem depends on definitions: df-bi 206 df-ral 3051 |
This theorem is referenced by: ralbiia 3080 ralcom3 3086 raleqbii 3327 ralrab 3685 raldifb 4141 raldifsni 4800 reusv2 5403 dfsup2 9474 iscard2 10006 acnnum 10082 dfac9 10166 dfacacn 10171 raluz2 12919 ralrp 13034 isprm4 16671 sdrgacs 20718 isdomn2 21280 isnrm2 23323 ismbl 25516 ellimc3 25869 dchrelbas2 27235 h1dei 31452 ralin 37870 fnwe2lem2 42622 |
Copyright terms: Public domain | W3C validator |