Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rexbidv2 | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 22-May-1999.) |
Ref | Expression |
---|---|
rexbidv2.1 | ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) |
Ref | Expression |
---|---|
rexbidv2 | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexbidv2.1 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) | |
2 | 1 | exbidv 1921 | . 2 ⊢ (𝜑 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒))) |
3 | df-rex 3147 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜓)) | |
4 | df-rex 3147 | . 2 ⊢ (∃𝑥 ∈ 𝐵 𝜒 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜒)) | |
5 | 2, 3, 4 | 3bitr4g 316 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∃wex 1779 ∈ wcel 2113 ∃wrex 3142 |
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 209 df-ex 1780 df-rex 3147 |
This theorem is referenced by: rexbidva 3299 rexeqbidv 3405 rexss 4041 exopxfr2 5718 isoini 7094 rexsupp 7851 omabs 8277 elfi2 8881 wemapsolem 9017 ltexpi 10327 rexuz 12301 ncoprmgcdne1b 15997 lpigen 20032 llyi 22085 nllyi 22086 elpi1 23652 xrecex 30600 bnj18eq1 32203 ldual1dim 36306 pmapjat1 36993 mrefg2 39310 islssfg2 39677 fourierdlem71 42469 hoiqssbl 42914 |
Copyright terms: Public domain | W3C validator |