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 1917 | . 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒))) |
3 | df-ral 3143 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
4 | df-ral 3143 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 316 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∀wal 1531 ∈ wcel 2110 ∀wral 3138 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 |
This theorem depends on definitions: df-bi 209 df-ral 3143 |
This theorem is referenced by: ralbidva 3196 raleqbidv 3402 ralss 4037 oneqmini 6237 ordunisuc2 7553 dfsmo2 7978 wemapsolem 9008 zorn2lem1 9912 raluz 12290 limsupgle 14828 ello12 14867 elo12 14878 lo1resb 14915 rlimresb 14916 o1resb 14917 isprm3 16021 isprm7 16046 ist1-2 21949 hausdiag 22247 xkopt 22257 cnflf 22604 cnfcf 22644 metcnp 23145 caucfil 23880 mdegleb 24652 islinds5 30927 eulerpartlemgvv 31629 filnetlem4 33724 mnuunid 40606 hoidmvle 42875 elbigo2 44605 |
Copyright terms: Public domain | W3C validator |