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 1737 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) |
3 | df-ral 2901 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
4 | df-ral 2901 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) | |
5 | 2, 3, 4 | 3bitr4i 291 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∀wal 1473 ∈ wcel 1977 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 |
This theorem depends on definitions: df-bi 196 df-ral 2901 |
This theorem is referenced by: ralbiia 2962 ralbii 2963 raleqbii 2973 ralrab 3335 raldifb 3712 raldifsni 4265 reusv2 4800 dfsup2 8233 iscard2 8685 acnnum 8758 dfac9 8841 dfacacn 8846 raluz2 11613 ralrp 11728 isprm4 15235 isdomn2 19120 isnrm2 20972 ismbl 23101 ellimc3 23449 dchrelbas2 24762 h1dei 27793 fnwe2lem2 36639 sdrgacs 36790 |
Copyright terms: Public domain | W3C validator |