![]() |
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 3177 | . 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | rexbidv 3178 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wral 3061 ∃wrex 3070 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-ral 3062 df-rex 3071 |
This theorem is referenced by: freq1 5645 rexfiuz 15290 cau3lem 15297 caubnd2 15300 climi 15450 rlimi 15453 o1lo1 15477 2clim 15512 lo1le 15594 caucvgrlem 15615 caurcvgr 15616 caucvgb 15622 vdwlem10 16919 vdwlem13 16922 pmatcollpw2lem 22270 neiptopnei 22627 lmcvg 22757 lmss 22793 elpt 23067 elptr 23068 txlm 23143 tsmsi 23629 ustuqtop4 23740 isucn 23774 isucn2 23775 ucnima 23777 metcnpi 24044 metcnpi2 24045 metucn 24071 xrge0tsms 24341 elcncf 24396 cncfi 24401 lmmcvg 24769 lhop1 25522 ulmval 25883 ulmi 25889 ulmcaulem 25897 ulmdvlem3 25905 pntibnd 27085 pntlem3 27101 pntleml 27103 axtgcont1 27708 perpln1 27950 perpln2 27951 isperp 27952 brbtwn 28146 uvtx01vtx 28643 isgrpo 29737 ubthlem3 30112 ubth 30113 hcau 30424 hcaucvg 30426 hlimi 30428 hlimconvi 30431 hlim2 30432 elcnop 31097 elcnfn 31122 cnopc 31153 cnfnc 31170 lnopcon 31275 lnfncon 31296 riesz1 31305 xrge0tsmsd 32196 signsply0 33550 unblimceq0 35371 cvgcau 44187 limcleqr 44346 addlimc 44350 0ellimcdiv 44351 climd 44374 climisp 44448 lmbr3 44449 climrescn 44450 climxrrelem 44451 climxrre 44452 xlimpnfxnegmnf 44516 xlimxrre 44533 xlimmnf 44543 xlimpnf 44544 xlimmnfmpt 44545 xlimpnfmpt 44546 dfxlim2 44550 cncfshift 44576 cncfperiod 44581 ioodvbdlimc1lem1 44633 ioodvbdlimc1lem2 44634 ioodvbdlimc2lem 44636 fourierdlem68 44876 fourierdlem87 44895 fourierdlem103 44911 fourierdlem104 44912 etransclem48 44984 |
Copyright terms: Public domain | W3C validator |