| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rexralbidv | Structured version Visualization version GIF version | ||
| Description: Formula-building rule for restricted quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.) |
| Ref | Expression |
|---|---|
| 2ralbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| Ref | Expression |
|---|---|
| rexralbidv | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2ralbidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 2 | 1 | ralbidv 3178 | . 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
| 3 | 2 | rexbidv 3179 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wral 3061 ∃wrex 3070 |
| 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-an 396 df-ex 1780 df-ral 3062 df-rex 3071 |
| This theorem is referenced by: freq1 5652 rexfiuz 15386 cau3lem 15393 caubnd2 15396 climi 15546 rlimi 15549 o1lo1 15573 2clim 15608 lo1le 15688 caucvgrlem 15709 caurcvgr 15710 caucvgb 15716 vdwlem10 17028 vdwlem13 17031 pmatcollpw2lem 22783 neiptopnei 23140 lmcvg 23270 lmss 23306 elpt 23580 elptr 23581 txlm 23656 tsmsi 24142 ustuqtop4 24253 isucn 24287 isucn2 24288 ucnima 24290 metcnpi 24557 metcnpi2 24558 metucn 24584 xrge0tsms 24856 elcncf 24915 cncfi 24920 lmmcvg 25295 lhop1 26053 ulmval 26423 ulmi 26429 ulmcaulem 26437 ulmdvlem3 26445 pntibnd 27637 pntlem3 27653 pntleml 27655 axtgcont1 28476 perpln1 28718 perpln2 28719 isperp 28720 brbtwn 28914 uvtx01vtx 29414 isgrpo 30516 ubthlem3 30891 ubth 30892 hcau 31203 hcaucvg 31205 hlimi 31207 hlimconvi 31210 hlim2 31211 elcnop 31876 elcnfn 31901 cnopc 31932 cnfnc 31949 lnopcon 32054 lnfncon 32075 riesz1 32084 xrge0tsmsd 33065 signsply0 34566 unblimceq0 36508 cvgcau 45501 limcleqr 45659 addlimc 45663 0ellimcdiv 45664 climd 45687 climisp 45761 lmbr3 45762 climrescn 45763 climxrrelem 45764 climxrre 45765 xlimpnfxnegmnf 45829 xlimxrre 45846 xlimmnf 45856 xlimpnf 45857 xlimmnfmpt 45858 xlimpnfmpt 45859 dfxlim2 45863 cncfshift 45889 cncfperiod 45894 ioodvbdlimc1lem1 45946 ioodvbdlimc1lem2 45947 ioodvbdlimc2lem 45949 fourierdlem68 46189 fourierdlem87 46208 fourierdlem103 46224 fourierdlem104 46225 etransclem48 46297 |
| Copyright terms: Public domain | W3C validator |