![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralimdv2 | Structured version Visualization version GIF version |
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.) |
Ref | Expression |
---|---|
ralimdv2.1 | ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐵 → 𝜒))) |
Ref | Expression |
---|---|
ralimdv2 | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimdv2.1 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐵 → 𝜒))) | |
2 | 1 | alimdv 1898 | . 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) → ∀𝑥(𝑥 ∈ 𝐵 → 𝜒))) |
3 | df-ral 3112 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
4 | df-ral 3112 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒)) | |
5 | 2, 3, 4 | 3imtr4g 297 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1523 ∈ wcel 2083 ∀wral 3107 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 |
This theorem depends on definitions: df-bi 208 df-ral 3112 |
This theorem is referenced by: ralimdva 3146 ssralv 3960 zorn2lem7 9777 pwfseqlem3 9935 sup2 11451 xrsupexmnf 12552 xrinfmexpnf 12553 xrsupsslem 12554 xrinfmsslem 12555 xrub 12559 r19.29uz 14548 rexuzre 14550 caurcvg 14871 caucvg 14873 isprm5 15884 prmgaplem5 16224 prmgaplem6 16225 mrissmrid 16745 elcls3 21379 iscnp4 21559 cncls2 21569 cnntr 21571 2ndcsep 21755 dyadmbllem 23887 xrlimcnp 25232 pntlem3 25871 sigaclfu2 30993 lfuhgr2 31975 rdgssun 34211 mapdordlem2 38325 dffltz 38789 iunrelexp0 39553 climrec 41447 0ellimcdiv 41493 |
Copyright terms: Public domain | W3C validator |