![]() |
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 1801 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) |
3 | df-ral 3110 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
4 | df-ral 3110 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) | |
5 | 2, 3, 4 | 3bitr4i 304 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∀wal 1520 ∈ wcel 2081 ∀wral 3105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 |
This theorem depends on definitions: df-bi 208 df-ral 3110 |
This theorem is referenced by: ralbiia 3131 ralbii 3132 raleqbii 3198 ralrab 3623 raldifb 4042 raldifsni 4635 reusv2 5195 dfsup2 8754 iscard2 9251 acnnum 9324 dfac9 9408 dfacacn 9413 raluz2 12146 ralrp 12259 isprm4 15857 sdrgacs 19270 isdomn2 19761 isnrm2 21650 ismbl 23810 ellimc3 24160 dchrelbas2 25495 h1dei 29018 fnwe2lem2 39136 |
Copyright terms: Public domain | W3C validator |