| 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 1920 | . 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒))) |
| 3 | df-ral 3062 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
| 4 | df-ral 3062 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒)) | |
| 5 | 2, 3, 4 | 3bitr4g 314 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐵 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 ∈ wcel 2108 ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-ral 3062 |
| This theorem is referenced by: ralbidva 3176 raleqbidv 3346 ralssOLD 4060 oneqmini 6436 ordunisuc2 7865 dfsmo2 8387 wemapsolem 9590 zorn2lem1 10536 raluz 12938 limsupgle 15513 ello12 15552 elo12 15563 lo1resb 15600 rlimresb 15601 o1resb 15602 isprm3 16720 isprm7 16745 ist1-2 23355 hausdiag 23653 xkopt 23663 cnflf 24010 cnfcf 24050 metcnp 24554 caucfil 25317 mdegleb 26103 islinds5 33395 islbs5 33408 eulerpartlemgvv 34378 filnetlem4 36382 mnuunid 44296 iineq12dv 45111 hoidmvle 46615 elbigo2 48473 ralbidb 48720 ralbidc 48721 |
| Copyright terms: Public domain | W3C validator |