| 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 1915 | . 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) → ∀𝑥(𝑥 ∈ 𝐵 → 𝜒))) | 
| 3 | df-ral 3061 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
| 4 | df-ral 3061 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒)) | |
| 5 | 2, 3, 4 | 3imtr4g 296 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∀wal 1537 ∈ wcel 2107 ∀wral 3060 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 | 
| This theorem depends on definitions: df-bi 207 df-ral 3061 | 
| This theorem is referenced by: ralimdva 3166 ssralvOLD 4055 zorn2lem7 10543 pwfseqlem3 10701 sup2 12225 xrsupexmnf 13348 xrinfmexpnf 13349 xrsupsslem 13350 xrinfmsslem 13351 xrub 13355 r19.29uz 15390 rexuzre 15392 caurcvg 15714 caucvg 15716 isprm5 16745 prmgaplem5 17094 prmgaplem6 17095 mrissmrid 17685 elcls3 23092 iscnp4 23272 cncls2 23282 cnntr 23284 2ndcsep 23468 dyadmbllem 25635 xrlimcnp 27012 pntlem3 27654 fldextrspunlsplem 33724 sigaclfu2 34123 lfuhgr2 35125 rdgssun 37380 mapdordlem2 41640 aks6d1c1 42118 sn-sup2 42506 dffltz 42649 cantnfresb 43342 safesnsupfiub 43434 iunrelexp0 43720 climrec 45623 0ellimcdiv 45669 pgindnf 49290 | 
| Copyright terms: Public domain | W3C validator |