Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ralbidva | GIF version |
Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 4-Mar-1997.) |
Ref | Expression |
---|---|
ralbidva.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
ralbidva | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1508 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | ralbidva.1 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | ralbida 2431 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∈ wcel 1480 ∀wral 2416 |
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 1423 ax-gen 1425 ax-4 1487 ax-17 1506 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-ral 2421 |
This theorem is referenced by: raleqbidva 2640 poinxp 4608 funimass4 5472 funimass3 5536 funconstss 5538 cocan1 5688 cocan2 5689 isocnv2 5713 isores2 5714 isoini2 5720 ofrfval 5990 ofrfval2 5998 dfsmo2 6184 smores 6189 smores2 6191 ac6sfi 6792 supisolem 6895 ordiso2 6920 ismkvnex 7029 caucvgsrlemcau 7601 suplocsrlempr 7615 axsuploc 7837 suprleubex 8712 dfinfre 8714 zextlt 9143 prime 9150 fzshftral 9888 fimaxq 10573 clim 11050 clim2 11052 clim2c 11053 clim0c 11055 climabs0 11076 climrecvg1n 11117 mertenslem2 11305 mertensabs 11306 dfgcd2 11702 sqrt2irr 11840 tgss2 12248 neipsm 12323 ssidcn 12379 lmbrf 12384 cnnei 12401 cnrest2 12405 lmss 12415 lmres 12417 ismet2 12523 elmopn2 12618 metss 12663 metrest 12675 metcnp 12681 metcnp2 12682 metcn 12683 txmetcnp 12687 divcnap 12724 elcncf2 12730 mulc1cncf 12745 cncfmet 12748 cdivcncfap 12756 limcdifap 12800 limcmpted 12801 cnlimc 12810 |
Copyright terms: Public domain | W3C validator |