Theorem r19.3rmv 3618

Description: Restricted quantification of wff not containing quantified variable. (Contributed by Jim Kingdon, 6-Aug-2018.)

Assertion

Ref	Expression
r19.3rmv	⊢ (∃𝑦 𝑦 ∈ 𝐴 → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑))

Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝜑,𝑥

Allowed substitution hint:   𝜑(𝑦)

Proof of Theorem r19.3rmv

Step	Hyp	Ref	Expression
1		nfv 1581	. 2 ⊢ Ⅎ𝑥𝜑
2	1	r19.3rm 3616	1 ⊢ (∃𝑦 𝑦 ∈ 𝐴 → (𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∃wex 1545   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-cleq 2231  df-clel 2234  df-ral 2533

This theorem is used by:  iinconstm  4021  exmidsssnc  4342  cnvpom  5333  ssfilem  7181  ssfilemd  7183  diffitest  7195  inffiexmid  7217  ctssexmid  7496  exmidonfinlem  7551  caucvgsrlemasr  8163  resqrexlemgt0  11808  rmodislmodlem  14796  rmodislmod  14797  rabid1o  17239  stnot  17244  wexmiddiffilem  17248  wexmiddifxylem  17250