![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralbidv2 | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 6-Apr-1997.) |
Ref | Expression |
---|---|
ralbidv2.1 | ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒))) |
Ref | Expression |
---|---|
ralbidv2 | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralbidv2.1 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐵 → 𝜒))) | |
2 | 1 | albidv 1924 | . 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒))) |
3 | df-ral 3063 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
4 | df-ral 3063 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 314 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1540 ∈ wcel 2107 ∀wral 3062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 df-ral 3063 |
This theorem is referenced by: ralbidva 3176 raleqbidv 3343 ralss 4055 oneqmini 6417 ordunisuc2 7833 dfsmo2 8347 wemapsolem 9545 zorn2lem1 10491 raluz 12880 limsupgle 15421 ello12 15460 elo12 15471 lo1resb 15508 rlimresb 15509 o1resb 15510 isprm3 16620 isprm7 16645 ist1-2 22851 hausdiag 23149 xkopt 23159 cnflf 23506 cnfcf 23546 metcnp 24050 caucfil 24800 mdegleb 25582 islinds5 32480 islbs5 32496 eulerpartlemgvv 33375 filnetlem4 35266 mnuunid 43036 hoidmvle 45316 elbigo2 47238 ralbidb 47485 ralbidc 47486 |
Copyright terms: Public domain | W3C validator |