Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rexralbidv | 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 2414 | . 2 ⊢ (𝜑 → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
3 | 2 | rexbidv 2415 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∀wral 2393 ∃wrex 2394 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-4 1472 ax-17 1491 ax-ial 1499 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-ral 2398 df-rex 2399 |
This theorem is referenced by: caucvgpr 7458 caucvgprpr 7488 caucvgsrlemgt1 7571 caucvgsrlemoffres 7576 axcaucvglemres 7675 cvg1nlemres 10725 rexfiuz 10729 resqrexlemgt0 10760 resqrexlemoverl 10761 resqrexlemglsq 10762 resqrexlemsqa 10764 resqrexlemex 10765 cau3lem 10854 caubnd2 10857 climi 11024 2clim 11038 ennnfonelemim 11864 lmcvg 12313 lmss 12342 txlm 12375 metcnpi 12611 metcnpi2 12612 elcncf 12656 cncfi 12661 limcimo 12730 cnplimclemr 12734 limccoap 12743 |
Copyright terms: Public domain | W3C validator |