![]() |
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 1815 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) |
3 | df-ral 3059 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
4 | df-ral 3059 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) | |
5 | 2, 3, 4 | 3bitr4i 303 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∀wal 1534 ∈ wcel 2105 ∀wral 3058 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 |
This theorem depends on definitions: df-bi 207 df-ral 3059 |
This theorem is referenced by: ralbiia 3088 ralcom3 3094 raleqbii 3341 ralrab 3701 raldifb 4158 raldifsni 4799 reusv2 5408 dfsup2 9481 iscard2 10013 acnnum 10089 dfac9 10174 dfacacn 10179 raluz2 12936 ralrp 13052 isprm4 16717 isdomn2OLD 20728 sdrgacs 20818 isnrm2 23381 ismbl 25574 ellimc3 25928 dchrelbas2 27295 h1dei 31578 iineq1i 36177 ixpeq1i 36181 ralin 38229 fnwe2lem2 43039 |
Copyright terms: Public domain | W3C validator |